Alternative Trace Axioms for the WHILE Construct

In NRL Report 9033 John McLean presents a programming language semantics, the extended trace language, based on the trace specification language. The simple programming language discussed in NRL Report 9033 contains the WHILE construct, and McLean gives this construct a natural and correct recursive treatment. This report shows that it is possible to use the extended trace language to give the WHILE construct two other quite different semantic treatments. One of these is based on the Hoare-style semantics for WHILE the second is an alternative to the recursive axiom that could be used in cases where the verifier can discern at what point a given loop will terminate. It is significant that when using the extended trace language a verifier of software can choose from several different but equivalent semantic treatments of WHILE. The ability to choose an axiom for WHILE that fits the problem at hand makes the extended trace language an attractive software verification formalism.