Program Semantics and Classical Logic



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



More intriguing information

1. Großhandel: Steigende Umsätze und schwungvolle Investitionsdynamik
2. Financial Market Volatility and Primary Placements
3. Firm Closure, Financial Losses and the Consequences for an Entrepreneurial Restart
4. Place of Work and Place of Residence: Informal Hiring Networks and Labor Market Outcomes
5. Opciones de política económica en el Perú 2011-2015
6. Who’s afraid of critical race theory in education? a reply to Mike Cole’s ‘The color-line and the class struggle’
7. Climate change, mitigation and adaptation: the case of the Murray–Darling Basin in Australia
8. Short report "About a rare cause of primary hyperparathyroidism"
9. CAN CREDIT DEFAULT SWAPS PREDICT FINANCIAL CRISES? EMPIRICAL STUDY ON EMERGING MARKETS
10. The name is absent