Program Semantics and Classical Logic

We see here that an assignment statement x := N is interpreted as the set
of pairs of input and output states such that input and output state differ
at most in the affected register and the value of the register in the output
state is the original value of N . The translation is clearly dependent upon
the Update Axiom. Tests B? are interpreted as sets of those pairs hi, ii such
that B is true in i. Program variables translate themselves; sequencing is
translated as relational composition; and choice is interpreted as union. The
recursion construct is interpreted as a simultaneous fixpoint. The interpre-
tation of hX_i ^ Piin=₁ (P) is obtained by considering all those assignments
to X1 , . . . , Xn for which it is the case that X1 = P1 and . . . and Xn = Pn are
all simultaneously true. For each of those assignments P will have a certain
value and we get the value of the whole construct by taking the intersection
of all values so obtained.

We give the translations of correctness formulas to conclude with. Trans-
lations are now of type t and are almost self-explanatory again. The interpre-
tation of the asserted program {F1}P {F2} expresses that after any successful
execution of P from a state where F₁ holds we shall be in a state where F₂
holds and ⊆, not unexpectedly, is interpreted as inclusion.

Definition 14 (Translation of Correctness Formulas)

({F1}P{F2})^t = ∀ij ((F₁^t(i) ∧ P⅜,ji)) → F2^t(j))        (17)

(Pi ⊆ P2)^t = ∀r (P^t(r) → P₂^t(r))                       (18)

7 Scott’s Induction Rule

The aim of this section is to import some conceptual machinery from the
Scott-Strachey tradition, adapt it to our revised setting, and develop the
necessary theory in this new setting. In particular, it will turn out to be
possible to prove the validity of Scott Induction, a rule which is immensely
useful when it comes to proving properties of programs containing the recur-
sion construct.

Our translation function f sends formulae to terms of type s → t, pro-
grams to s × s → t terms and correctness formulae to terms of type t. Clearly,
the domains corresponding to these terms come with natural Boolean alge-
bras: if F is of type α → t then F is the characteristic function of a set RF ,
which may be identified with F itself. This means that Dα→t corresponds to

16

<<   13   14   15   16   17   18   19   >>

More intriguing information