Definition 1 (Language)
|
Num : |
:= 0 | |
S(Num) | |
|
N: |
:= x | |
Num | |
N1 + N2 | N1 × N2 |
|
B: |
:= false |
| N1 = |
N2 | N1 ≤ N2 | B1 → B2 |
|
F: |
:= B | |
F1 → F2 |
| ∀xF |
|
A: |
:= x := N |
| B? |
|X |
|
P: |
:= A | |
P1;P2 |
Pi ∪ P2 | hXi ^ Piin=ι(p) |
|
C: |
:= {F1}P {F2} | |
P1 ⊆ P2 | |
Note that the construction hXi ^ Pi)n=1(P), unlike the similar construct
studied in [3], may be nested to an arbitrary depth. A real programming
language such as PASCAL would write hXi ^ Piin=1(P) as follows.
procedure X1 ;
P1;
procedure Xn ;
P
n;
P
This exhausts our stock of programs. The category C finally, consists of cor-
rectness statements, which can be divided into asserted programs {F1}P {F2}
stating that program P , whenever it is started in a state where F1 holds, will
after any successful execution be in a state where F2 holds. The statement
P1 ⊆ P2 expresses that if we can reach a state j starting from a state i by
running P1 , we can also get from i to j by running P2.
The following abbreviations are useful.
|
Definition 2 (Abbreviations) | |||
|
true |
is |
short for |
false → false |
|
-F |
is |
short for |
F → false |
|
F1 ∨ F2 |
is |
short for |
-F1 → F2 |
|
F1 ∧ F2 |
is |
short for |
-(-Fi ∨ -F2) |
|
∃xF |
is |
short for |
-Vx-F |
|
N1 < N2 |
is |
short for |
N1 ≤ N2 ∧ -N1 = N2 |
5