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. Modelling the health related benefits of environmental policies - a CGE analysis for the eu countries with gem-e3
2. The name is absent
3. Legal Minimum Wages and the Wages of Formal and Informal Sector Workers in Costa Rica
4. The name is absent
5. The Demand for Specialty-Crop Insurance: Adverse Selection and Moral Hazard
6. The name is absent
7. CHANGING PRICES, CHANGING CIGARETTE CONSUMPTION
8. Sustainability of economic development and governance patterns in water management - an overview on the reorganisation of public utilities in Campania, Italy, under EU Framework Directive in the field of water policy (2000/60/CE)
9. The Impact of Individual Investment Behavior for Retirement Welfare: Evidence from the United States and Germany
10. ROBUST CLASSIFICATION WITH CONTEXT-SENSITIVE FEATURES