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=1 (P) is obtained by considering all those assignments
to X
1 , . . . , 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 {F
1}P {F2} expresses that after any successful
execution of P from a state where F
1 holds we shall be in a state where F2
holds and , not unexpectedly, is interpreted as inclusion.

Definition 14 (Translation of Correctness Formulas)

({F1}P{F2})t = ij ((F1t(i) P⅜,ji)) → F2t(j))        (17)

(Pi P2)t = r (Pt(r) → P2t(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 R
F ,
which may be identified with F itself. This means that D
α→t corresponds to

16



More intriguing information

1. Ultrametric Distance in Syntax
2. EMU: some unanswered questions
3. Evaluating the Success of the School Commodity Food Program
4. POWER LAW SIGNATURE IN INDONESIAN LEGISLATIVE ELECTION 1999-2004
5. Pupils’ attitudes towards art teaching in primary school: an evaluation tool
6. The name is absent
7. GENE EXPRESSION AND ITS DISCONTENTS Developmental disorders as dysfunctions of epigenetic cognition
8. Changing spatial planning systems and the role of the regional government level; Comparing the Netherlands, Flanders and England
9. The name is absent
10. Migrating Football Players, Transfer Fees and Migration Controls
11. Stable Distributions
12. From Communication to Presence: Cognition, Emotions and Culture towards the Ultimate Communicative Experience. Festschrift in honor of Luigi Anolli
13. Modelling Transport in an Interregional General Equilibrium Model with Externalities
14. From music student to professional: the process of transition
15. Self-Help Groups and Income Generation in the Informal Settlements of Nairobi
16. The Macroeconomic Determinants of Volatility in Precious Metals Markets
17. A Theoretical Growth Model for Ireland
18. The name is absent
19. The name is absent
20. Optimal Rent Extraction in Pre-Industrial England and France – Default Risk and Monitoring Costs