Floyd-Hoare Logic

Info

Floyd-Hoare logic is a formal system with a set of logical rules for reasoning rigorously about the correctness of a computer program.

We will use a Mickey Mouse programming language that has assignments to integers and booleans.

Example program:

    State: X = ?, Y = ?
X := 2,
    State: X = 2, Y = ?
Y := 1
    State: X = 2, Y = 1
X := X + 1
    State: X = 3, Y = 1
Y := Y + X
    State: X = 3, Y = 4
Properties

Proof theories for program correctness are usually sound (sometimes unsound is faster, and we have a tolerance).

Most often, they are not complete (by Gödel's Incompleteness Theorem, there is no complete proof theory for arithmetic, and we often manipulate numbers in a program).

Hoare Triple

Definition

A formal verification argument is a three-triple , and we prove arguments in the form:

assert(P);
C;
assert(Q);

where:

  • is the precondition
  • is the program
  • is the postcondition

Other common notations: (| P |) C (| Q |) or {P}C{Q}.

Every assertion (except the precondition) needs justification.

Partial and Total Correctness

Partial Correctness

Definition

|= par assert(P); C; assert(Q);

means that for all program executions of that start in a state satisfying precondition (i.e the program is valid), if the execution terminates, then at termination postcondition is satisfied in the final state.

We usually only care about partial correctness, because the Halting Problem is undecitdable.

Total Correctness

Definition

|= tot assert(P); C; assert(Q)y

means for all program states that satisfy precondition , is guaranteed to terminate and the resulting state satisfies the postcondition .

History Variables

Definition

History variables (also known as auxiliary/ghost/shadow/logical variables) are variables that do not appear in the program, but refer to the value of a program at some point in the past.

Example

We can spec the following program using :

assert(x >= 0); // Don't technically need this for partial correctness

y := 1;
z := 0;

while !(z = x) do {
    z := z + 1;
    y := y * z;
}

assert(y = fact(x));

However, we cannot do the same with this program, since it "consumes" . We need a history variable.

assert(x = x0 & x > 0);
y := 1;

while !(x = 0) do {
    y := y * x;
    x := x - 1;
}

assert(y = fact(x0));

Proof Rules

Assignments

Axiom

Written vertically:

Intuitively, we have to look at these rules backwards (i.e bottom up). The bottom rule is in terms of , while the top rule has substituted in for . In other words, denotes the assertion in which each free occurrence of was replaced with .

Examples

assert(y > 0);
x := y;
assert(x > 0); // by asn

assert(2 = y);
x := 2;
assert(x = y); // by asn

assert(2 > 0);
x := 2;
assert(X > 0); // by asn

assert(x + 1 = 2);
x := x + 1;
assert(x = 2); // by asn

assert(0 < x + 1 & x + 1 < 10)
x := x + 1
assert(0 < x & x < 10); // by asn

assert(z = x + y + 1 - 4);
x := x + y + 1;
assert(z = x - 4); // by asn

Sequences of Commands

Rule

Example

Specify and prove a program that swaps the variables and in a program.

spec

assert(y = y0 & x = x0);
r := x;
x := y;
y := r;
assert(x = y0 & y = x0);

proof

assert(y = y0 & x = x0);
r := x;
assert(y = y0 & r = x0); // by asn

assert(y = y0 & r = x0);
x := y;
assert(x = y0 & r = x0); // by asn

assert(x = y0 & r = x0);
y := r;
assert(x = y0 & y = x0); // by asn

We can chain matching post-pre conditions:

assert(y = y0 & x = x0);
r := x;
assert(y = y0 & r = x0); // by asn
x := y;
assert(x = y0 & r = x0); // by asn
y := r;
assert(x = y0 & y = x0); // by asn
Tip

Work backwards from the postcondition to the precondition

Implied Proof Rule

Rule

and are verification conditions which must be proven separately

Example

Prove the partial correctness of the program:

assert(x >= 5 & y >= 0);
z := x;
z := z + y;
u := z;
assert(u >= 5); // by asn

proof

assert(x >= 5 & y >= 0);
assert(x + y >= 5); // by implied on VC1
z := x;
assert(z + y >= 5); // by asn
z := z + y;
assert(z >= 5); // by asn
u := z;
assert(u >= 5); // by asn

VC1:

We must also prove every verification condition. This one is quite trivial. Using Natural Deduction and the Theory of Natural Number Arithmetic:

Strength of Pre and Post Conditions

Definition

In or , we say is stronger than , and is weaker than .

Definition

When we know , and , and we conclude , this is called precondition strengthening. We are assuming more in the precondition than we need to prove the program satisfies the postcondition.

When we know , and , and we conclude , this is called postcondition weakening. We are concluding less in the postcondition than what is actually true in the program.

Example

Prove that the following program is correct:

func main() {
    assert(f = fib(k) & g = fib(k - 1) & k >= 1);
    t := g;
    g := f;
    f := f + t;
    k := k + 1;
    assert(f = fib(k) & g = fib(k - 1));
}

proof

func main() {
    assert(f = fib(k) & g = fib(k - 1) & k >= 1);
    assert(f + g = fib(k = 1) & f = fib(k)) by implied on VC1;
    t := g;
    assert(f + t = fib(k + 1) & f = fib(k)) by asn;
    g := f;
    assert(f + t = fib(k + 1) & g = fib(k)) by asn;
    f := f + t;
    assert(f = fib(k + 1) & g = fib(k)) by asn;
    k := k + 1;
    assert(f = fib(k) & g = fib(k - 1));
}

VC: verification condition

proof

One-Armed Conditional

Rule

We need to prove 2 things:

Written horizontally:

assert(P);

if B then {
    assert(P & B) by if_then;
    C;
    assert(Q) by Proof_Rule;
};

assert(Q) by if_then on VC1;

VC1:

Example

Prove the correctness of the program:

assert(true)

if (max < B) then {
    max := B;
};

assert(max >= B)

proof

assert(true)

if (max < B) then {
    assert(max < B) by if_then;
    assert(B >= B) by implied using arith;
    max := B;
    assert(max >= B) by asn;
};

assert(max >= B) by if_then on VC1;

VC1: by arith

Two-Armed Conditional

Rule

We need to prove 2 things:

Written horizontally:

assert(P)

if B then {
    assert(P & B) by if_then_else;
    C1;
    assert(Q) by Proof_Rule; 
} else {
    assert(P & !B) by if_then_else;
    C2;
    assert(Q) by Proof_Rule;
};

assert(Q) by if_then_else;
Example

Prove the correctness of the program:

assert(true);
a := x + 1;

if (a - 1 = 0) then {
    y := 1;
} else {
    y := a;
};

assert(y = x + 1);

proof

assert(true);
assert(x + 1 = x + 1) by implied using eq_i;
a := X + 1
assert(a = x + 1) by asn;

if (a - 1 = 0) then {
    assert((a = x + 1) & (a - 1 = 0)) by if_then_else;
    assert(1 = x + 1) by implied on VC1;
    y := 1;
    assert(y = x + 1) by asn;
} else {
    assert((a = x + 1) & !(a - 1 = 0)) by if_then_else;
    assert(a = x + 1) by implied on VC1;
    y := a;
    assert(y = x + 1) by asn;
};

assert(y = x + 1) by if_then_else;

VC1:
this proof is trivial.

Derived Two-Armed Conditional

Rule

Derived if-then-else proof rule, which allows us to work backwards, copy Q, then find , then write the top line.

assert((B => P1) & (!B => P2))

if B then {
    assert(P1) by if_then_else;
    C1;
    assert(Q) by Proof_Rule; 
} else {
    assert(P2) by if_then_else;
    C2;
    assert(Q) by Proof_Rule;
};

assert(Q) by if_then_else;

Why this works:

assert((B => P1) & (!B => P2));

if B then {
    assert((B => P1) & (!B => P2) & B) by if_then_else;
    assert(P1) by implied on VC1;
    C1;
    assert(Q) by Proof_Rule; 
} else {
    assert((B => P1) & (!B => P2) & !B) by if_then_else;
    assert(P2) by implied on VC2;
    C2;
    assert(Q) by Proof_Rule;
};

assert(Q) by if_then_else;

and we have two VCs that are easy to prove:
VC1:
VC2:

Example

Prove the correctness of the program:

assert(x >= 4);
y := x;
x := x - 2;

if (x >= 4) then {
    y := 1;
} else {
    x := 0 - 3;
};

assert(x + y >= 2);

solution

assert(x >= 5);
assert(x - 2 < 4 => x >= 5) by implied on VC1;
y := x;
x := x - 2;
assert(x < 4 => y >= 5)
assert((x >= 4 => x >= 1) & (!(x >= 4) = y >= 5))

if (x >= 4) then {
    assert(x >= 1) by if_then_else;
    assert(x + 1 >= 2) by implied using arith;
    y := 1;
    assert(x + y >= 2) by asn;
} else {
    assert(y >= 5) by if_then_else;
    assert(0 - 3 + y >= 2) by implied using arith;
    x := 0 - 3;
    assert(x + y >= 2) by asn;
};

assert(x + y >= 2) by if_then_else;

VC1:
VC2:

Make sure you prove these.

While Loops

Rule

We need to prove:

Written horizontally:

where Inv is loop invariant

assert(P);
assert(Inv) by implied on VC1;

while B do {
    assert(Inv & B) by partial_while;
    C;
    assert(Inv) by Proof_Rule;
};
assert(Inv & !B) by partial_while;
assert(Q) by implied on VC2;

Loop invariant: Inv
VC1:
VC2:

The invariant is a wff (assertion) that the program state satisfies before and after each execution of the loop body . Note that the invariant is not unique, but we want to find the smallest formula that works.

Note

Find an such that:

  1. (the inv is strong enough to prove the postcondition)
  2. (is an invariant)
  3. (the invariant is not stronger than the precondition)
Example

Prove the correctness of the following program:

assert(true);
y := 1;
z := 0;

while (z != x) do {
    z := z + 1;
    y := z * y;
};

assert(y = fact(x));

proof
Finding the loop invariant:
Suppose . Then:
0 1 true
1 1 true
2 true
3 true
4 false

Candidate loop invariant: 

assert(true);
assert(1 = fact(0)) implied using artih; // defn of factorial
y := 1;
assert(y = fact(0)) by asn;
z := 0;
assert(y = fact(z)) by asn;

while !(z = x) do {
    assert(y = fact(z) & !(z = x)) by partial_while;
    assert((z + 1) * y = fact(z + 1) by implied on VC1;
    z := z + 1;
    assert(z * y = fact(z)) by asn;
    y := z * y;
    assert(y = fact(z)) by asn;
};

assert(y = fact(z) & z = x) by partial_while
assert(y = fact(x)) by implied on VC2;

Loop invariant:
VC1:
VC2:

todo show steps

Example

Prove the correctness of the following program:

assert(0 <= n & a > 0);
s := 1;
i := 0;

while (i < n) do {
    s := s * a;
    i := i + 1;
};

assert(s = a^n);

solution
Finding the loop invariant:
Suppose and , then:
0 true
1 true
2 true
3 true

Candidate loop invariant:
VC3:

If we try to prove VC3, we will get stuck:

So we need as our loop invariant, and VC3: :

assert(0 <= n & a > 0);
assert(1 = a^0 & 0 <= n) by implied on VC1;
s := 1;
assert(s = a^0 & 0 <= n) by asn;
i := 0;
assert(s = a^i & i <= n) by asn;

while (i < n) do {
    assert(s = a^i & i <= n & i < n) by partial_while;
    assert(s * a = a^(i + 1) & i + 1 <= n) by implied on VC2;
    s := s * a;
    assert(s = a^(i + 1) & i + 1 <= n) by asn;
    i := i + 1;
    assert(s = a^i & i <= n) by asn;
};

assert(s = a^i & i <= n & !(i < n)) by partial_while;
assert(s = a^n) by implied on VC3;

VC2:

VC1:

Example

Prove the correctness of the following program:

assert(x >= 0 & x = x0);
y := 0;

while (x != 0) do {
    y := y + 1;
    x := x - 1;
};

assert(y = x0);

proof

assert(x >= 0 & x = x0);
assert(0 = x0 - x) by implied on VC1;
y := 0;
assert(y = x0 - x) by asn;

while (x != 0) do {
    assert(y = x0 - x & x != 0) by partial_while;
    assert(y + 1 = x0 - (x - 1)) by implied on VC2;
    y := y + 1;
    assert(y = x0 - (x - 1)) by asn;
    x := x - 1;
    assert(y = x0 - x) by asn;
};

assert(y = x0 - x & x = 0) by partial_while;
assert(y = x0) by implied on VC3;

Loop invariant:
VC1:

VC2:

VC3:

Arrays

assert(A[y] = 0)
A[x] := 1;
assert(A[y] = 0)

this is wrong. If then this is false. You have to consider the entire array.

Think of arrays as functional binary relations, pair of index and data.

Assigning to one index of the array is a special case of relational overriding:

Array assignment rule:

[!example]
Consider the program:

B[k] := 14;
assert(B[4] = C);

what must be true before this program runs?

If , then
Otherwise, .

In proofs of VCs, we see this used in three ways:

& (18)\quad i = j \
& (19)\quad B \oplus { (i, e) }[i] = e & \text{by set on 18 // override}
\end

\begin{align}
& (25)\quad sus
\end

You can't use 'macro parameter character #' in math mode ### Functions Formal parameters: used in the definition Actual parameters: used in the call A function returns a value and thins value is used in an expression ```go func f(x1, x2) { assert(R); C; assert(S); return ret; }; ``` Function rule: A particular WFF is a tautology for this program. Use this tautology to prove VCs. For the function call $f(a_{1}, a_{2}, \dots, a_{n})$:

\begin{align}
& \op{assert}
\end

(R \implies S)\big[ a_{1}/x_{1}, a_{2}/x_{2}, \dots, a_{n}/x_{n}, f(a_{1}, a_{2}, \dots, a_{n})/\text{ret} \big]

b \ge 0, \quad b \ge 0 \implies f(b, c) = b + c \quad \vdash \quad f(b, c) \ge b + c

i = i_{0}, \quad \op{inc}(i) = i + 1, \quad \op{inc}(i + 2) = i + 2 + 1 \quad \vdash \quad \op{inc}(\op{inc}(i) + 1) = 10 + 3

\begin{align}
& (1)\quad i = i_{0} && \text{premise} \
& (\text{lem1})\quad \op{inc}(i) = i + 1 && \text{premise} \
& (\text{lem2})\quad \op{inc}(i + 2) = i + 2 = 1 && \text{premise} \
& (4)\quad \op{inc}(\op{inc}(i) + 1) = \op{inc}(\op{inc}(i) + 1) && \text{by eq_i} \
& (5)\quad \op{inc}(\op{inc}(i) + 1) = \op{inc}(i + 1 + 1) && \text{by eq_e on lem1, 4} \
& (6)\quad \op{inc}(\op{inc}(i) + 1) = \op{inc}(i + 2) && \text{by arith on 5} \
& (7)\quad \op{inc}(\op{inc}(i) + 1) = i + 2 + 1 && \text{by eq_e on lem2, 6} \
& (8)\quad \op{inc}(\op{inc}(i) + 1) = i + 3 && \text{by arith on 7} \
& (9)\quad \op{inc}(\op{inc}(i) + 1) = i_{0} + 3 && \text{by eq_e on 1, 8} \
& \QED
\end

Misplaced &[!example] ```go func inc(x) { assert(x = x0); x := x + 1; assert(x = x0 + 1); } assert(b = b0); inc(b); inc(b); assert(b = b0 + 2) ``` ```go func inc(x) { assert(x = x0); x := x + 1; assert(x = x0 + 1); } assert(b = b0); inc(b); assert(b = b0 = 1) by procedure; assert(b + b1 & b1 = b0 + 1) by hist_var_intro; inc(b); assert(b = b1 + 1 & b1 = b0 + 1) by procedure; assert(b = b0 + 2) by implied on VC1; ``` VC1: $b = b_{1} + 1 \land b_{1} = b_{0} + 1 \vdash b = b_{0} = 2$ #### Function Termination [!example] Linear search: Pre: $\exists k \cdot 0 \le k \land k \le i \land B[k] = c$ ```go func find(i) { assert(Pre); if (B[i] = c) then { assert(Pre & B[i] = c) by if_then_else; assert(B[i] = c) by implied using and_e; ret := i; assert(B[ret] = c) by asn; } else { assert(Pre & !(B[i] = c)) by if_then_else; assert(B[find(i - 1)] = c) by implied on VC1; ret := find(i - 1); assert(B[ret] = c) by asn; } assert(B[ret] = c) } ``` VC1: $\big( \exists k \cdot 0 \le k \land k \le i \land B[k] = c \big) \land \neg(B[i] = c) \vdash B[\op{find}(i - 1)] = c$

\begin{align}
& (1)\quad \big( \exists k \cdot 0 \le k \land k \le i \land B[k] = c \big) \land \neg(B[i] = c) \
& (1)\quad \exists k \cdot 0 \le k \land k \le i \land B[k] = c && \text{by and_e on 1} \
& (2)\quad \neg(B[i] = c) && \text{by and_e on 1}
\end

Misplaced & [!example] Goofy ahh program ```go func add(x, y) { assert((x = x0) & (y >= 0)); if (y != 0) then { assert(x = x0 & y >= 0 & y != 0) by if_then; assert(x = x0 & (y - 1 >= 0)) by implied on VC1; add(x, y - 1); assert(x = x0 + y - 1) by procedure; assert(x + 1 = x0 + y) by implied on arith; x := x + 1; assert(x = x0 + y) by asn; } assert(x = x0 + y) by if_then on VC2; } ``` Vc2: $x = x_{0} \land y \ge 0 \land y = 0 \vdash x = x_{0} + y$ ## While loop Termination To show total termination of a while-loop, show that the loop terminates. Identify an integer expression involving the variables of the loop condition whose value: 1. is always greater than 0 2. decreases with every loop iteration, and 3. makes the loop's guard becomes false as it approaches 0 [!example] ```js assert(n > 0) sum := 0; j := 0; while (j != n) do { sum := sum + a; j := j + 1; }; ``` Bounding function is $n - j$ because: - $n > 0$ is in the precondition and $j = 0$ at the beginning, so $n - j > 0$ - [!example] Pre: $\exists k \cdot 0 \le k \land k \le i \land B[k] = c$ ```go func find(i) { assert(Pre); if (B[i] = c) then { ret := i; } else { ret} } ``` [!example] ```go func add(x, y) { assert((x = x0) & (y >= 0)); if (y != 0) then { add(x, y - 1); x := x + 1; } } ```