Program Semantics and Classical Logic

the intended behaviour of our programs and in fact P₁ 'C P₂ will imply that
an execution of P₁ is also a possible way of executing P₂ . Section 4 gives a
short overview of classical type logic (of which we shall use only the second-
order part) and section 5 introduces the necessary axiomatic extension. One
restriction on our class of models will be that we shall want a certain do-
main De to behave like the natural numbers, to which end we shall adopt
the (second-order) Peano axioms. Another constraint will be that we want
a domain D_s to act like a set of program states . This will be achieved by
adopting a first-order axiom. The actual translation of the programming lan-
guage then follows in section 6. Section 7 imports the concepts of continuity,
anticontinuity and monotonicity from the usual Scott approach, develops
some theory, and proves that Scott’s Induction Rule holds within the present
setting. Section 8 introduces the usual Hoare calculus for our programming
language and proves it to be sound relative to the semantics of section 6.
The main theorem of the paper then follows in section 9: We define a linear
program as a program which is just a sequence of atomic statements and, for
any program P, consider all linear programs L such that L 'C P. It turns
out that the denotation of P , given our semantics, is exactly the union of the
denotations of all such L.

2 A Toy Programming Language

The programming language which we shall study in this paper is defined by
the Backus-Naur form in definition 1, which is almost self-explanatory. The
set Num consists of the numerals 0, S(0), S(S(0)),. . ., which we shall write
in decimal notation. N consists of arithmetical terms built out of numerals
and first-order variables. In B we find Boolean combinations of equalities
and inequalities built up from these terms, and F is essentially the language
of first order arithmetic. The set A consists of assignment statements x := N,
tests B?, and program variables, or procedure calls X . The category P extends
this set by allowing sequencing, choice and, the most important programming
construct in this paper, recursion. We allow a set of procedure declarations
hX₁ ^ P₁,..., Xn ^ Pni, abbreviated hXi ^ Piin=₁, or even hXi ^ Piii, to
bind the program variables X₁ , . . . , X_n in a given program P. The variables
X1 , . . . , Xn may occur free (for the definition of free occurrence see below) in
P1 , . . . , Pn, so that procedure declarations may call one another.

<<   1   2   3   4   5   6   7   >>

More intriguing information