Core Programming Language

Hoare Triples; Partial and Total Correctness

Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

11—Program Verification

CS 3234: Logic and Formal Systems

Martin Henz and Aquinas Hobor

October 29, 2009

Generated on Thursday 29th October, 2009, 13:52

CS 3234: Logic and Formal Systems 11—Program Verification 1

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 2

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation

Model checking is bumping into major problems, if the

systems deal with complex data structures and numbers,
and interact with the user and each other in complex ways.

CS 3234: Logic and Formal Systems 11—Program Verification 3

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation

Model checking is bumping into major problems, if the

systems deal with complex data structures and numbers,
and interact with the user and each other in complex ways.
Models become infinite.

CS 3234: Logic and Formal Systems 11—Program Verification 4

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation

Model checking is bumping into major problems, if the

systems deal with complex data structures and numbers,
and interact with the user and each other in complex ways.
Models become infinite.
Satisfaction/validity becomes undecidable.

CS 3234: Logic and Formal Systems 11—Program Verification 5

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation

Model checking is bumping into major problems, if the

systems deal with complex data structures and numbers,
and interact with the user and each other in complex ways.
Models become infinite.
Satisfaction/validity becomes undecidable.
We retreat to a proof-based framework for software
program verification.

CS 3234: Logic and Formal Systems 11—Program Verification 6

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Characteristics of the Approach

Proof-based instead of model checking

CS 3234: Logic and Formal Systems 11—Program Verification 7

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Characteristics of the Approach

Proof-based instead of model checking

Semi-automatic instead of automatic

CS 3234: Logic and Formal Systems 11—Program Verification 8

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Characteristics of the Approach

Proof-based instead of model checking

Semi-automatic instead of automatic
Property-oriented not using full specification

CS 3234: Logic and Formal Systems 11—Program Verification 9

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Characteristics of the Approach

Proof-based instead of model checking

Semi-automatic instead of automatic
Property-oriented not using full specification
Application domain fixed to sequential programs using integers

CS 3234: Logic and Formal Systems 11—Program Verification 10

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Characteristics of the Approach

Proof-based instead of model checking

Semi-automatic instead of automatic
Property-oriented not using full specification
Application domain fixed to sequential programs using integers
Interleaved with development rather than a-posteriori
verification

CS 3234: Logic and Formal Systems 11—Program Verification 11

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Reasons for Program Verification

Documentation. Program properties formulated as theorems

can serve as concise documentation

CS 3234: Logic and Formal Systems 11—Program Verification 12

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Reasons for Program Verification

Documentation. Program properties formulated as theorems

can serve as concise documentation
Time-to-market. Verification prevents/catches bugs and can
reduce development time

CS 3234: Logic and Formal Systems 11—Program Verification 13

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Reasons for Program Verification

Documentation. Program properties formulated as theorems

can serve as concise documentation
Time-to-market. Verification prevents/catches bugs and can
reduce development time
Reuse. Clear specification provides basis for reuse

CS 3234: Logic and Formal Systems 11—Program Verification 14

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Reasons for Program Verification

Documentation. Program properties formulated as theorems

can serve as concise documentation
Time-to-market. Verification prevents/catches bugs and can
reduce development time
Reuse. Clear specification provides basis for reuse
Certification. Verification is required in safety-critical domains
such as nuclear power stations and aircraft
cockpits

CS 3234: Logic and Formal Systems 11—Program Verification 15

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Framework for Software Verification

Convert informal description R of requirements for an

application domain into formula φR .

CS 3234: Logic and Formal Systems 11—Program Verification 16

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Framework for Software Verification

Convert informal description R of requirements for an

application domain into formula φR .
Write program P that meets φR .

CS 3234: Logic and Formal Systems 11—Program Verification 17

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Framework for Software Verification

Convert informal description R of requirements for an

application domain into formula φR .
Write program P that meets φR .
Prove that P satisfies φR .

CS 3234: Logic and Formal Systems 11—Program Verification 18

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Framework for Software Verification

Convert informal description R of requirements for an

application domain into formula φR .
Write program P that meets φR .
Prove that P satisfies φR .
Each step provides risks and opportunities.

CS 3234: Logic and Formal Systems 11—Program Verification 19

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 20

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation of Core Language

Real-world languages are quite large; many features and

constructs

CS 3234: Logic and Formal Systems 11—Program Verification 21

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation of Core Language

Real-world languages are quite large; many features and

constructs
Verification framework would exceed time we have in
CS3234

CS 3234: Logic and Formal Systems 11—Program Verification 22

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation of Core Language

Real-world languages are quite large; many features and

constructs
Verification framework would exceed time we have in
CS3234
Theoretical constructions such as Turing machines or
lambda calculus are too far from actual applications; too
low-level

CS 3234: Logic and Formal Systems 11—Program Verification 23

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation of Core Language

Real-world languages are quite large; many features and

constructs
Verification framework would exceed time we have in
CS3234
Theoretical constructions such as Turing machines or
lambda calculus are too far from actual applications; too
low-level
Idea: use subset of Pascal/C/C++/Java

CS 3234: Logic and Formal Systems 11—Program Verification 24

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Motivation of Core Language

Real-world languages are quite large; many features and

constructs
Verification framework would exceed time we have in
CS3234
Theoretical constructions such as Turing machines or
lambda calculus are too far from actual applications; too
low-level
Idea: use subset of Pascal/C/C++/Java
Benefit: we can study useful “realistic” examples

CS 3234: Logic and Formal Systems 11—Program Verification 25

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Expressions in Core Language

Expressions come as arithmetic expressions E:

E ::= n | x | (−E) | (E + E) | (E − E) | (E ∗ E)

CS 3234: Logic and Formal Systems 11—Program Verification 26

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Expressions in Core Language

Expressions come as arithmetic expressions E:

E ::= n | x | (−E) | (E + E) | (E − E) | (E ∗ E)

and boolean expressions B:

B ::= true | false | (!B) | (B&B) | (BkB) | (E < E)

CS 3234: Logic and Formal Systems 11—Program Verification 27

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Expressions in Core Language

Expressions come as arithmetic expressions E:

E ::= n | x | (−E) | (E + E) | (E − E) | (E ∗ E)

and boolean expressions B:

B ::= true | false | (!B) | (B&B) | (BkB) | (E < E)

Where are the other comparisons, for example ==?

CS 3234: Logic and Formal Systems 11—Program Verification 28

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Commands in Core Language

Commands cover some common programming idioms.

Expressions are components of commands.

C ::= x = E | C; C | if B {C} else {C} | while B {C}

CS 3234: Logic and Formal Systems 11—Program Verification 29

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

Consider the factorial function:

def
0! = 1
def
(n + 1)! = (n + 1) · n!

We shall show that after the execution of the following Core

program, we have y = x!.
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

CS 3234: Logic and Formal Systems 11—Program Verification 30

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 31

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

CS 3234: Logic and Formal Systems 11—Program Verification 32

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

We need to be able to say that at the end, y is x!

CS 3234: Logic and Formal Systems 11—Program Verification 33

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

We need to be able to say that at the end, y is x!

That means we require a post-condition y = x!

CS 3234: Logic and Formal Systems 11—Program Verification 34

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

Do we need pre-conditions, too?

CS 3234: Logic and Formal Systems 11—Program Verification 35

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

Do we need pre-conditions, too?

Yes, they specify what needs to be the case before
execution.
Example: x > 0

CS 3234: Logic and Formal Systems 11—Program Verification 36

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

Do we need pre-conditions, too?

Yes, they specify what needs to be the case before
execution.
Example: x > 0
Do we have to prove the postcondition in one go?

CS 3234: Logic and Formal Systems 11—Program Verification 37

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

Do we need pre-conditions, too?

Yes, they specify what needs to be the case before
execution.
Example: x > 0
Do we have to prove the postcondition in one go?
No, the postcondition of one line can be the
pre-condition of the next!

CS 3234: Logic and Formal Systems 11—Program Verification 38

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Assertions on Programs

Shape of assertions

(|φ|) P (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 39

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Assertions on Programs

Shape of assertions

(|φ|) P (|ψ|)

Informal meaning
If the program P is run in a state that satisfies φ, then the state
resulting from P’s execution will satisfy ψ.

CS 3234: Logic and Formal Systems 11—Program Verification 40

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

(Slightly Trivial) Example

Informal specification
Given a positive number x, the program P calculates a number
y whose square is less than x.

CS 3234: Logic and Formal Systems 11—Program Verification 41

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

(Slightly Trivial) Example

Informal specification
Given a positive number x, the program P calculates a number
y whose square is less than x.

Assertion
(|x > 0|) P (|y · y < x|)

CS 3234: Logic and Formal Systems 11—Program Verification 42

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

(Slightly Trivial) Example

Informal specification
Given a positive number x, the program P calculates a number
y whose square is less than x.

Assertion
(|x > 0|) P (|y · y < x|)

Example for P
y = 0

CS 3234: Logic and Formal Systems 11—Program Verification 43

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

(Slightly Trivial) Example

Informal specification
Given a positive number x, the program P calculates a number
y whose square is less than x.

Assertion
(|x > 0|) P (|y · y < x|)

Example for P
y = 0

Our first Hoare triple

(|x > 0|) y = 0 (|y · y < x|)

CS 3234: Logic and Formal Systems 11—Program Verification 44
 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

(Slightly Less Trivial) Example

Same assertion
(|x > 0|) P (|y · y < x|)

Another example for P

y = 0;
while ( y ∗ y < x ) {
y = y + 1;
}
y = y − 1;

CS 3234: Logic and Formal Systems 11—Program Verification 45

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Recall: Models in Predicate Logic

Definition
Let F contain function symbols and P contain predicate
symbols. A model M for (F, P) consists of:
1 A non-empty set A, the universe;
2 for each nullary function symbol f ∈ F a concrete element
f M ∈ A;
3 for each f ∈ F with arity n > 0, a concrete function
f M : An → A;
4 for each P ∈ P with arity n > 0, a set P M ⊆ An .

CS 3234: Logic and Formal Systems 11—Program Verification 46

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Recall: Satisfaction Relation

The model M satisfies φ with respect to environment l, written

M |=l φ:
in case φ is of the form P(t1 , t2 , . . . , tn ), if the result
(a1 , a2 , . . . , an ) of evaluating t1 , t2 , . . . , tn with respect to l is
in P M ;
in case φ has the form ∀xψ, if the M |=l[x7→a] ψ holds for all
a ∈ A;
in case φ has the form ∃xψ, if the M |=l[x7→a] ψ holds for
some a ∈ A;

CS 3234: Logic and Formal Systems 11—Program Verification 47

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Recall: Satisfaction Relation (continued)

in case φ has the form ¬ψ, if M |=l ψ does not hold;

in case φ has the form ψ1 ∨ ψ2 , if M |=l ψ1 holds or
M |=l ψ2 holds;
in case φ has the form ψ1 ∧ ψ2 , if M |=l ψ1 holds and
M |=l ψ2 holds; and
in case φ has the form ψ1 → ψ2 , if M |=l ψ1 holds
whenever M |=l ψ2 holds.

CS 3234: Logic and Formal Systems 11—Program Verification 48

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Hoare Triples

Definition
An assertion of the form (|φ|) P (|ψ|) is called a Hoare triple.
φ is called the precondition, ψ is called the postcondition.
A state of a Core program P is a function l that assigns
each variable x in P to an integer l(x).
A state l satisfies φ if M |=l φ, where M contains integers
and gives the usual meaning to the arithmetic operations.
Quantifiers in φ and ψ bind only variables that do not occur
in the program P.

CS 3234: Logic and Formal Systems 11—Program Verification 49

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

Let l(x) = −2, l(y) = 5 and l(z) = −1. We have:

l |= ¬(x + y < z)
l 6|= y = x · z < z
l 6|= ∀u(y < u → y · z < u · z)

CS 3234: Logic and Formal Systems 11—Program Verification 50

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Partial Correctness

Definition
We say that the triple (|φ|) P (|ψ|) is satisfied under partial
correctness if, for all states which satisfy φ, the state resulting
from P’s execution satisfies ψ, provided that P terminates.

CS 3234: Logic and Formal Systems 11—Program Verification 51

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Partial Correctness

Definition
We say that the triple (|φ|) P (|ψ|) is satisfied under partial
correctness if, for all states which satisfy φ, the state resulting
from P’s execution satisfies ψ, provided that P terminates.

Notation
We write |=par (|φ|) P (|ψ|).

CS 3234: Logic and Formal Systems 11—Program Verification 52

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Extreme Example

(|φ|) while true { x = 0; } (|ψ|)

holds for all φ and ψ.

CS 3234: Logic and Formal Systems 11—Program Verification 53

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Total Correctness

Definition
We say that the triple (|φ|) P (|ψ|) is satisfied under total
correctness if, for all states which satisfy φ, P is guaranteed to
terminate and the resulting state satisfies ψ.

Notation
We write |=tot (|φ|) P (|ψ|).

CS 3234: Logic and Formal Systems 11—Program Verification 54

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Back to Factorial

Consider Fac1:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

CS 3234: Logic and Formal Systems 11—Program Verification 55

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Back to Factorial

Consider Fac1:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

|=tot (|x ≥ 0|) Fac1 (|y = x!|)

CS 3234: Logic and Formal Systems 11—Program Verification 56

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Back to Factorial

Consider Fac1:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

|=tot (|x ≥ 0|) Fac1 (|y = x!|)

6|=tot (|⊤|) Fac1 (|y = x!|)

CS 3234: Logic and Formal Systems 11—Program Verification 57

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Back to Factorial

Consider Fac1:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

|=tot (|x ≥ 0|) Fac1 (|y = x!|)

6|=tot (|⊤|) Fac1 (|y = x!|)
|=par (|x ≥ 0|) Fac1 (|y = x!|)

CS 3234: Logic and Formal Systems 11—Program Verification 58

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Back to Factorial

Consider Fac1:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }

|=tot (|x ≥ 0|) Fac1 (|y = x!|)

6|=tot (|⊤|) Fac1 (|y = x!|)
|=par (|x ≥ 0|) Fac1 (|y = x!|)
|=par (|⊤|) Fac1 (|y = x!|)

CS 3234: Logic and Formal Systems 11—Program Verification 59

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 60

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Strategy

We are looking for a proof calculus that allows us to establish

⊢par (|φ|) P (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 61

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Strategy

We are looking for a proof calculus that allows us to establish

⊢par (|φ|) P (|ψ|)

where
|=par (|φ|) P (|ψ|) holds whenever ⊢par (|φ|) P (|ψ|)
(correctness)

CS 3234: Logic and Formal Systems 11—Program Verification 62

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Strategy

We are looking for a proof calculus that allows us to establish

⊢par (|φ|) P (|ψ|)

where
|=par (|φ|) P (|ψ|) holds whenever ⊢par (|φ|) P (|ψ|)
(correctness), and
⊢par (|φ|) P (|ψ|) holds whenever |=par (|φ|) P (|ψ|)
(completeness).

CS 3234: Logic and Formal Systems 11—Program Verification 63

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness

(|φ|) C1 (|η|) (|η|) C2 (|ψ|)

[Composition]
(|φ|) C1 ; C2 (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 64

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness (continued)

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 65

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

CS 3234: Logic and Formal Systems 11—Program Verification 66

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:

CS 3234: Logic and Formal Systems 11—Program Verification 67

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|2 = 2|) P (|x = 2|)

CS 3234: Logic and Formal Systems 11—Program Verification 68

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|2 = 2|) P (|x = 2|)
(|2 = 4|) P (|x = 4|)

CS 3234: Logic and Formal Systems 11—Program Verification 69

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|2 = 2|) P (|x = 2|)
(|2 = 4|) P (|x = 4|)
(|2 = y|) P (|x = y|)

CS 3234: Logic and Formal Systems 11—Program Verification 70

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Examples

Let P be the program x = 2.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|2 = 2|) P (|x = 2|)
(|2 = 4|) P (|x = 4|)
(|2 = y|) P (|x = y|)
(|2 > 0|) P (|x > 0|)

CS 3234: Logic and Formal Systems 11—Program Verification 71

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

More Examples

Let P be the program x = x + 1.

CS 3234: Logic and Formal Systems 11—Program Verification 72

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

More Examples

Let P be the program x = x + 1.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:

CS 3234: Logic and Formal Systems 11—Program Verification 73

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

More Examples

Let P be the program x = x + 1.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|x + 1 = 2|) P (|x = 2|)

CS 3234: Logic and Formal Systems 11—Program Verification 74

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

More Examples

Let P be the program x = x + 1.

Using

[Assignment]
(|[x → E]ψ|) x = E (|ψ|)

we can prove:
(|x + 1 = 2|) P (|x = 2|)
(|x + 1 = y|) P (|x = y|)

CS 3234: Logic and Formal Systems 11—Program Verification 75

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness (continued)

(|φ ∧ B|) C1 (|ψ|) (|φ ∧ ¬B|) C2 (|ψ|)

[If-statement]
(|φ|) if B { C1 } else { C2 } (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 76

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness (continued)

(|φ ∧ B|) C1 (|ψ|) (|φ ∧ ¬B|) C2 (|ψ|)

[If-statement]
(|φ|) if B { C1 } else { C2 } (|ψ|)

(|ψ ∧ B|) C (|ψ|)

[Partial-while]
(|ψ|) while B { C } (|ψ ∧ ¬B|)

CS 3234: Logic and Formal Systems 11—Program Verification 77

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness (continued)

⊢AR φ′ → φ (|φ|) C (|ψ|) ⊢AR ψ → ψ ′

[Implied]
(|φ′ |) C (|ψ ′ |)

CS 3234: Logic and Formal Systems 11—Program Verification 78

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Proof Tableaux
Proofs have tree shape
All rules have the structure

something

something else

As a result, all proofs can be written as a tree.

Practical concern
These trees tend to be very wide when written out on paper.
Thus we are using a linear format, called proof tableaux.
CS 3234: Logic and Formal Systems 11—Program Verification 79
 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Interleave Formulas with Code

(|φ|) C1 (|η|) (|η|) C2 (|ψ|)

[Composition]
(|φ|) C1 ; C2 (|ψ|)
Shape of rule suggests format for proof of C1 ; C2 ; . . . ; Cn :
(|φ0 |)
C1 ;
(|φ1 |) justification
C2 ;
..
.
(|φn−1 |) justification
Cn ;
(|φn |) justification
CS 3234: Logic and Formal Systems 11—Program Verification 80
 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Working Backwards

Overall goal
Find a proof that at the end of executing a program P, some
condition ψ holds.

CS 3234: Logic and Formal Systems 11—Program Verification 81

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Working Backwards

Overall goal
Find a proof that at the end of executing a program P, some
condition ψ holds.

Common situation
If P has the shape C1 ; . . . ; Cn , we need to find the weakest
formula ψ ′ such that
(|ψ ′ |) Cn (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 82

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Working Backwards

Overall goal
Find a proof that at the end of executing a program P, some
condition ψ holds.

Common situation
If P has the shape C1 ; . . . ; Cn , we need to find the weakest
formula ψ ′ such that
(|ψ ′ |) Cn (|ψ|)

Terminology
The weakest formula ψ ′ is called weakest precondition.

CS 3234: Logic and Formal Systems 11—Program Verification 83

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

(|y < 3|)

(|y + 1 < 4|) Implied
y = y + 1;
(|y < 4|) Assignment

CS 3234: Logic and Formal Systems 11—Program Verification 84

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Another Example

Can we claim u = x + y after z = x; z = z + y; u = z; ?

CS 3234: Logic and Formal Systems 11—Program Verification 85

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Another Example

Can we claim u = x + y after z = x; z = z + y; u = z; ?

(|⊤|)
(|x + y = x + y|) Implied
z = x;
(|z + y = x + y|) Assignment
z = z + y;
(|z = x + y|) Assignment
u = z;
(|u = x + y|) Assignment

CS 3234: Logic and Formal Systems 11—Program Verification 86

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

An Alternative Rule for If

We have:

(|φ ∧ B|) C1 (|ψ|) (|φ ∧ ¬B|) C2 (|ψ|)

[If-statement]
(|φ|) if B { C1 } else { C2 } (|ψ|)

Sometimes, the following derived rule is more suitable:

(|φ1 |) C1 (|ψ|) (|φ2 |) C2 (|ψ|)

[If-stmt 2]
(|(B → φ1 ) ∧ (¬B → φ2 )|) if B { C1 } else { C2 } (|ψ|)

CS 3234: Logic and Formal Systems 11—Program Verification 87

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Example

Consider this implementation of Succ:

a = x + 1;
i f ( a = 1 == 0 ) {
y = 1;
} else {
y = a;
}
Can we prove (|⊤|) Succ (|y = x + 1|) ?

CS 3234: Logic and Formal Systems 11—Program Verification 88

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Another Example

..
.
if ( a − 1 == 0 ) {
(|1 = x + 1|) If-Statement 2
y = 1;
(|y = x + 1|) Assignment
} else {
(|a = x + 1|) If-Statement 2
y = a;
(|y = x + 1|) Assignment
}
(|y = x + 1|) If-Statement 2

CS 3234: Logic and Formal Systems 11—Program Verification 89

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Another Example
(|⊤|)
(|(x + 1 − 1 = 0 → 1 = x + 1)∧
(¬(x + 1 − 1 = 0) → x + 1 = x + 1)|) Implied
a = x + 1;
(|(a − 1 = 0 → x + 1)∧
(¬(a − 1 = 0) → a = x + 1)|) Assignment
if ( a − 1 == 0 ) {
(|1 = x + 1|) If-Statement 2
y = 1;
(|y = x + 1|) Assignment
} else {
(|a = x + 1|) If-Statement 2
y = a;
(|y = x + 1|) Assignment
CS 3234: Logic and Formal Systems 11—Program Verification 90
 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Recall: Partial-while Rule

(|ψ ∧ B|) C (|ψ|)

[Partial-while]
(|ψ|) while B { C } (|ψ ∧ ¬B|)

CS 3234: Logic and Formal Systems 11—Program Verification 91

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Factorial Example

We shall show that the following Core program Fac1 meets this
specification:
y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }
Thus, to show:
(|⊤|) Fac1 (|y = x!|)

CS 3234: Logic and Formal Systems 11—Program Verification 92

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Partial Correctness of Fac1

..
.
(|y = z!|)
while ( z != x ) {
(|y = z! ∧ z 6= x|) Invariant
(|y · (z + 1) = (z + 1)!|) Implied
z = z + 1;
(|y · z = z!|) Assignment
y = y ∗ z;
(|y = z!|) Assignment
}
(|y = z! ∧ ¬(z 6= x)|) Partial-while
(|y = x!|) Implied

CS 3234: Logic and Formal Systems 11—Program Verification 93

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Partial Correctness of Fac1

(|⊤|)
(|(1 = 0!)|) Implied
y = 1;
(|y = 0!|) Assignment
z = 0;
(|y = z!|) Assignment
while ( z != x ) {
..
.
}
(|y = z! ∧ ¬(z 6= x)|) Partial-while
(|y = x!|) Implied

CS 3234: Logic and Formal Systems 11—Program Verification 94

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 95

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Ideas for Total Correctness

The only source of non-termination is the while

command.
If we can show that the value of an integer expression
decreases in each iteration, but never goes negative, we
have proven termination.

CS 3234: Logic and Formal Systems 11—Program Verification 96

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Ideas for Total Correctness

The only source of non-termination is the while

command.
If we can show that the value of an integer expression
decreases in each iteration, but never goes negative, we
have proven termination.
Why?

CS 3234: Logic and Formal Systems 11—Program Verification 97

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Ideas for Total Correctness

The only source of non-termination is the while

command.
If we can show that the value of an integer expression
decreases in each iteration, but never goes negative, we
have proven termination.
Why? Well-foundedness of natural numbers

CS 3234: Logic and Formal Systems 11—Program Verification 98

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Ideas for Total Correctness

The only source of non-termination is the while

command.
If we can show that the value of an integer expression
decreases in each iteration, but never goes negative, we
have proven termination.
Why? Well-foundedness of natural numbers
We shall include this argument in a new version of the
while rule.

CS 3234: Logic and Formal Systems 11—Program Verification 99

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Rules for Partial Correctness (continued)

(|ψ ∧ B|) C (|ψ|)

[Partial-while]
(|ψ|) while B { C } (|ψ ∧ ¬B|)

(|ψ ∧ B ∧ 0 ≤ E = E0 |) C (|ψ ∧ 0 ≤ E < E0 |)

[Total-while]
(|ψ ∧ 0 ≤ E|) while B { C } (|ψ ∧ ¬B|)

CS 3234: Logic and Formal Systems 11—Program Verification 100

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Factorial Example (Again!)

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }
What could be a good invariant?

CS 3234: Logic and Formal Systems 11—Program Verification 101

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Factorial Example (Again!)

y = 1;
z = 0;
while ( z ! = x ) { z = z + 1 ; y = y ∗ z ; }
What could be a good invariant?

Answer:
x −z

CS 3234: Logic and Formal Systems 11—Program Verification 102

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Total Correctness of Fac1

..
.
(|y = z! ∧ 0 ≤ x − z|)
while ( z != x ) {
(|y = z! ∧ z 6= x ∧ 0 ≤ x − z = E0 |) Invariant
(|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 6= x)|) Total-while
(|y = x!|) Implied

CS 3234: Logic and Formal Systems 11—Program Verification 103

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Total Correctness of Fac1

(|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 6= x)|) Total-while
(|y = x!|) Implied

CS 3234: Logic and Formal Systems 11—Program Verification 104

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

1 Core Programming Language

2 Hoare Triples; Partial and Total Correctness

3 Proof Calculus for Partial Correctness

4 Proof Calculus for Total Correctness

5 Programming by Contract

CS 3234: Logic and Formal Systems 11—Program Verification 105

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Programming by Contract

Consider
(|φ|) P (|ψ|)

Obligation for consumer of P

Only run P when φ is met.

Obligation for producer of P

Make sure ψ is met after every run of P, assuming that φ is met
before the run.

CS 3234: Logic and Formal Systems 11—Program Verification 106

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Contracts as Documentation

i n t f a c t o r i a l ( x : i n t ) { . . . return y ; }
Method name: factorial
Input: x of type int
Assumes: 0≤x
Guarantees: y = x!
Output: y
Modifies only: y

CS 3234: Logic and Formal Systems 11—Program Verification 107

 Core Programming Language
Hoare Triples; Partial and Total Correctness
Proof Calculus for Partial Correctness
Proof Calculus for Total Correctness
Programming by Contract

Next Week

Lecture 12: Semantics of Hoare Logic

CS 3234: Logic and Formal Systems 11—Program Verification 108