KEMBAR78
Hoare Triple and Program Verification - Handout | PDF
Scribd
Upload
80 views12 pages

Hoare Triple and Program Verification - Handout

The document discusses Hoare triples and program verification. It defines partial correctness and total correctness of Hoare triples using the notation (|φ|) P (|ψ|) where φ is the precondition, P is a program, and ψ is the postcondition. An example program to calculate a factorial is shown and proven partially and totally correct using proof rules and invariants.

Uploaded by

Hưng Phạm
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
80 views12 pages

Hoare Triple and Program Verification - Handout

The document discusses Hoare triples and program verification. It defines partial correctness and total correctness of Hoare triples using the notation (|φ|) P (|ψ|) where φ is the precondition, P is a program, and ψ is the postcondition. An example program to calculate a factorial is shown and proven partially and totally correct using proof rules and invariants.

Uploaded by

Hưng Phạm
Copyright
© © All Rights Reserved
We take content rights seriously. If you suspect this is your content, claim it here.
Available Formats
Download as PDF, TXT or read online on Scribd
You are on page 1/ 12

Hoare triple

&
Program verification

Thinh Tien Nguyen, Ph.D.


Online lecture
Hoare triple

Definition:
(|ϕ|) P (|ψ|)
● ϕ: precondition
● ψ: postcondition
● P: a certain program

Ex:
(|x + 1 = y|) x = x + 1 (|x = y|)
Partial correctness

Definition:
For all states satisfying ϕ, assume that P actually terminates, if the
state resulting from P’s execution satisfies ψ, the Hoare triple
(|ϕ|) P (|ψ|)
is partially correct

Notation:
⊨par(|ϕ|) P (|ψ|)
Partial correctness

Program P:
y=1;
z=0;
while (z != x){
z = z + 1;
y = y * z;
}

⊨par(|T|) P (|y = x!|)


Total correctness

Definition:
For all states satisfying ϕ, if P terminates and the state resulting
from P’s execution satisfies ψ, the Hoare triple
(|ϕ|) P (|ψ|)
is totally correct

Notation:
⊨tot(|ϕ|) P (|ψ|)
Total correctness

Program P:
y=1;
z=0;
while (z != x){
z = z + 1;
y = y * z;
}

⊨tot(|x≥0|) P (|y = x!|)


Proof rules
Proof rules

Program P:
y=1;
z=0;
while (z != x){
z = z + 1;
y = y * z;
}

⊦par(|T|) P (|y = x!|)


Proof rules
(|T|)
(|1 = 0!|) Implied
y=1;
(|y = 0!|) Assignment
z=0;
(|y = z!|) Assignment
while (z != x) {
(|y = z! ∧ z != x|) Invariant Hyp. ∧ Guard
(|y * (z + 1) = (z + 1)!|) Implied
z = z + 1;
(|y * z = z!|) Assignment
y = y * z;
(|y = z!|) Assignment
}
(|y = z! ∧ z = x|) Partial while
(|y = x!|) Implied
Comments on total correctness

Program P:
y=1;
z=0;
while (z != x){
z = z + 1;
y = y * z;
}

⊦tot(|x≥0|) P (|y = x!|)


Comments on total correctness
Comments on total correctness
(|x≥0|)
(|1 = 0! ∧ 0 ≤ x - 0|) Implied
y=1;
(|y = 0! ∧ 0 ≤ x – 0|) Assignment
z=0;
(|y = z! ∧ 0 ≤ x – z |) Assignment
while (z != x){
(|y = z! ∧ z != x ∧ 0 ≤ x – z = E0|) Invariant Hyp. ∧ Guard
(|y * (z + 1) = (z + 1)! ∧ 0 ≤ x – (z + 1) < E0|) Implied
z = z + 1;
(|y * z = z! ∧ 0 ≤ x - z < E0|) Assignment
y = y * z;
(|y = z! ∧ 0 ≤ x - z < E0|) Assignment
}
(|y = z! ∧ z = x |) Total while
(|y = x!|) Implied

You might also like