The core idea of the RISC ProgramExplorer is to translate every program into its “semantic essence”, i.e. a declarative form that exhibits all that is to be known about the program from the mathematical point of view. This semantics is exhibited to the user for investigation and analysis (programming and specification errors may so be detected early); it also represents the basis for the subsequent verification of the program. Given a method
with specification fs and body c, c is translated into a formula fc which describes the effect of c; the proof that the method satisfies its specification is then essentially the proof of
fc ⇒ fs
i.e., that the effect of c implies the specification.
In somewhat more detail, we translate every program command (e.g. the body of a program method) into a logic formula that describes the relationship between the value of every program variable x in the prestate of the execution (this value is in the formula denoted as old x) to the value of the variable in the poststate (this value is denoted as var x). For instance, the program command
is translated to the formula (the state relation)
var x = old x+old y
This formula, however, does not explicitly say anything about the variables whose values are not changed (y,z,…) such that the post-state value of such variables is undefined. To overcome this problem, we additionally determine the frame of the variable which is the set of program variables that may be changed by the command. For above command, the program frame would be just x, from which we can deduce
var y = old y∧var z = old z∧…
i.e., var v = old v, for every program variable v different from x.
A sequence of commands
is handled by first translating the individual commands to state relations
var y = old y+1∧var x = old x
var x = old x+old y∧var y = old y
with common frame x,y. These formulas are then combined to a single state relation
∃x0,y0 :
y0 = old y+1∧x0 = old x ∧
var x = x0 +y0 ∧var y = y0
where x0,y0 represent the values of the program variables after the execution of the first command; these values are not visible as pre/post-state values of the combined command and therefore “hidden” by existential quantification. The combined formula can then be logically simplified by inserting the definitions of these values. This results in the state relation
var x = old x+old y+1∧var y = old y+1
with frame x,y.
Likewise, a local variable declaration
is translated to a state relation of form
∃x0,x1 : fc[x0∕old x,x1∕var x]
where fc denotes the state relation of c; in this formula, all references to old x respectively var x are substituted by references to existentially quantified variables x0 respectively y0. A conditional command
is translated to a statue relation
if fe then f1 else f2
(which is syntactic sugar for (fe ⇒ f1)∧(¬fe ⇒ f2)) where fe,f1,f2 denote the translations of e,c1,c2. Finally, a while loop
is translated to the state relation
f ∧¬fe′
i.e. a loop invariant just denotes (an upper bound approximation of) the loop’s state relation; the formula fe′ describes that the value of e in the poststate is false.
The translation of program commands to state relations is more thoroughly discussed in Appendix A; in the following we present its application to some sample programs.