Program Semantics and Classical Logic



the intended behaviour of our programs and in fact P1 'C P2 will imply that
an execution of
P1 is also a possible way of executing P2 . 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
Ds 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
hX1 ^ P1,..., Xn ^ Pni, abbreviated hXi ^ Piin=1, or even hXi ^ Piii, to
bind the program variables
X1 , . . . , Xn 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.



More intriguing information

1. The name is absent
2. Types of Tax Concessions for Promoting Investment in Free Economic and Trade Areas
3. The name is absent
4. The name is absent
5. The name is absent
6. How much do Educational Outcomes Matter in OECD Countries?
7. ‘Goodwill is not enough’
8. The name is absent
9. The name is absent
10. An Incentive System for Salmonella Control in the Pork Supply Chain
11. Achieving the MDGs – A Note
12. Wage mobility, Job mobility and Spatial mobility in the Portuguese economy
13. Testing the Information Matrix Equality with Robust Estimators
14. The name is absent
15. The name is absent
16. Kharaj and land proprietary right in the sixteenth century: An example of law and economics
17. I nnovative Surgical Technique in the Management of Vallecular Cyst
18. The name is absent
19. Who is missing from higher education?
20. 03-01 "Read My Lips: More New Tax Cuts - The Distributional Impacts of Repealing Dividend Taxation"