Program Semantics and Classical Logic



Corollary 14 (Scott’s Induction Rule) Assume X1, . . . , Xn are not free
in C. Write C(Q) for [Q/X]C. Then

C ([fail/Xi,..., fail∕Xn]P )+
X111.Xn(C(P)^→C∖[Pι∕Xι,11.,Pn∕Xn]Pr AX
C
(hXi ^ Pi)i(P))+

8 Hoare’s Calculus

As a simple application we show that our semantics subsumes the Hoare
Calculus, which we shall present in Gentzen form. Sequents Γ
'h C will
consist of a set of asserted programs Γ and an asserted program C. The
derivability relation
'PA between assertions F is given by an axiomatization
of first-order logic plus the first-order Peano axioms. Structural rules of our
Hoare-Gentzen calculus are the following.

C 'h C


Γι 'h C


Γι, Γ2 'h C


Γι 'h Ci Γ2,C1 'h C2
γ1, γ2 'h C2


(Id)

(Weakening)

(Cut)


The following logical rules embody the Hoare Calculus.

'H {[N∕x]F}x := N{F}


(Assignment)


'H {F}B?{F B}               (Test)

Γi 'h {F1}P1{F2} Γ2 'h {F2}P2{F3}

Γι, Γ2 'h {Fi}Pi; P2{F3}

Γι 'h {F1}P1{F2} Γ2 'h {F1}P2{F2}
Γι, Γ2 'h {F1}P1 P2{F2}

Γ 'H {F1}[fail∕X1,..., fail∕Xn]P {F2}

Γ, {Fι}P{F2} 'h {F1}[P1∕X1,..., Pn/Xn]P{F2}

Γ 'h {F}lXi ^ Pi)n,l(P){F2}

(Composition)

(Choice)

(Recursion)


Fi 'PA F2 Γ 'h {F2}P{F3} F3 'PA F4
Γ 'h {Fi}P{F4}

(Consequence)


24



More intriguing information

1. Industrial Employment Growth in Spanish Regions - the Role Played by Size, Innovation, and Spatial Aspects
2. Can genetic algorithms explain experimental anomalies? An application to common property resources
3. Cryothermal Energy Ablation Of Cardiac Arrhythmias 2005: State Of The Art
4. Evidence on the Determinants of Foreign Direct Investment: The Case of Three European Regions
5. Handling the measurement error problem by means of panel data: Moment methods applied on firm data
6. Population ageing, taxation, pensions and health costs, CHERE Working Paper 2007/10
7. The name is absent
8. The ultimate determinants of central bank independence
9. The name is absent
10. INTERACTION EFFECTS OF PROMOTION, RESEARCH, AND PRICE SUPPORT PROGRAMS FOR U.S. COTTON