10 Hoare Logic

Lecture from: 25.10.2024 | Video: Videos ETHZ

Hoare Logic - Reasoning about Program Correctness

Hoare logic provides a formal framework for verifying program correctness. Its core concept is the Hoare triple, denoted {P} S {Q}, where:

• P: Precondition – an assertion about the program state before executing program segment S.
• S: Program segment – a sequence of one or more statements.
• Q: Postcondition – an assertion about the program state after executing S.

A Hoare triple is valid if whenever P is true before the execution of S, and S terminates, then Q is true after the execution of S.

A really good explanation and recap…

Forward and Backward Reasoning

Two primary reasoning strategies exist for establishing Hoare triples:

1. Forward Reasoning (Deductive Verification)

Starts with the precondition and traces the program’s execution, deriving assertions after each statement until reaching a postcondition. It answers the question: Given this precondition, what postcondition can be guaranteed?

Example:

{u > 0}                     // Precondition
x = 17;
{u > 0 ∧ x == 17}           // After x = 17
y = 42;
{u > 0 ∧ x == 17 ∧ y == 42}  // After y = 42
z = u + x + y;
{u > 0 ∧ x == 17 ∧ y == 42 ∧ z == u + 59} // After z = u + x + y
// Consequently: {z > 59}

2. Backward Reasoning (Goal-Oriented Verification)

Starts with the desired postcondition and works backward through the program, deriving necessary preconditions for each statement. It answers the question: What precondition is needed to guarantee this postcondition?

Example:

{u + 17 + 42 > 59}        // Working backward from postcondition z > 59
z = u + x + y;              // with x = 17 and y = 42
{z > 59}                     // Postcondition
 
// Simplifying: {u > 0}

Comparison

Assignment Rules

For assignment statements, the Hoare triple takes the following form:

{P} X = E {Q}

Where:

• $P$ is the precondition: A logical assertion that must be true before the assignment is executed.
• $X=E$ is the assignment statement, assigning the value of expression $E$ to variable $X$.
• $Q$ is the postcondition: A logical assertion that will be true after the assignment is executed.

To prove the validity of this triple, we use the following substitution rule:

1. Replace all occurrences of $X$ in $Q$ with $E$, resulting in $Q^{\prime }$.
2. Demonstrate that the implication $P⟹Q^{\prime }$ holds. In other words, if $P$ is true, then $Q^{\prime }$ must also be true.

Rationale:

Let’s break down why this rule works:

1. We want to ensure that the postcondition $Q$ is true after the assignment $X=E$.
2. The assignment changes only the value of $X$ to $E$; everything else in the program’s state remains unchanged. Therefore, if $Q$ is true after the assignment, then a modified version of $Q$ where $X$ is replaced by $E$ (i.e., $Q^{\prime }$) must have been true before the assignment.
3. By showing that $P⟹Q^{\prime }$, we are demonstrating that $P$ is a sufficiently strong precondition to guarantee that $Q^{\prime }$ was true before the assignment, and thus $Q$ will be true afterwards.

Rules for Program Segments

When dealing with sequential program segments, we apply Hoare Logic to each segment individually and then connect them. Consider two consecutive Hoare triples:

{P1} S1 {Q1}
{P2} S2 {Q2}

To establish the validity of the combined segment:

{P1}
S1;
S2;
{Q2}

We must fulfill two conditions:

1. Prove the validity of each individual triple: {P1} S1 {Q1} and {P2} S2 {Q2}.
2. Demonstrate the implication $Q1⟹P2$. This ensures that the postcondition of $S1$ satisfies the precondition of $S2$, establishing a proper flow of logical correctness.

Example:

Let’s analyze the following example using backward reasoning (rückwärtsschliessen):

{x > 0} y = x + 1; z = y * y {z > y}

We decompose this into two separate triples:

{x > 0}
y = x + 1;
{y > 1}
z = y * y
{z > y}

1. Triple 1: $\{x>0\}y=x+1\{y>1\}$ is valid. Applying the assignment rule, we replace $y$ with $x+1$ in the postcondition, yielding $x+1>1$. Simplifying, we get $x>0$, which is our precondition. Since $x>0⟹x>0$, the triple is valid.

2. Triple 2: $\{y>1\}z=y\ast y\{z>y\}$ is valid. Replacing $z$ with $y\ast y$ in the postcondition gives $y\ast y>y$. Since $y>1$, this inequality holds. Since $y>1⟹y\ast y>y$, the second triple is also valid.

3. Finally, since both individual triples are valid and $y>1$ (Q1) implies $y>1$ (P2), the entire segment is valid.

Weak vs. Strong Statements

Assertions vary in strength. P1 is stronger than P2 (and P2 is weaker than P1) if P1 ⇒ P2. Stronger preconditions are harder to satisfy but provide more information. Stronger postconditions offer more guarantees.

Examples:

{a > 0 ∧ b > 0}             // A1 - Stronger Precondition
x = a / b;
{x > 0}
 
{a + b > 0}                // A2 - Weaker Precondition
x = a + b;
{x > 0}
 
 
{true}                      // B1 - Weaker Postcondition
x = y + 1;
{x > y}
 
{true}                      // B2 - Stronger Postcondition
x = y + 1;
{x == y + 1}

• $A1$ has a stronger precondition than $A2$ because $(a>0\wedge b>0)⟹(a+b>0)$.
• $B2$ has a stronger postcondition than $B1$ because $(x==y+1)⟹(x>y)$.

From a code user’s perspective, weaker preconditions are easier to satisfy, while stronger postconditions provide more guarantees. Conversely, code developers often find stronger preconditions and weaker postconditions easier to establish during program development.

Rules for Conditional Statements

Conditional statements introduce branching logic. Consider a conditional statement within a Hoare triple:

{P} if (b) S1 else S2 {Q}

Or, equivalently:

{P}
if (b) {
  S1;
} else {
  S2;
}
{Q}

This triple is valid if and only if both of the following triples are valid:

1. $\{P\wedge b\}S1\{Q\}$: If the precondition $P$ and the condition $b$ are true, then executing $S1$ must result in the postcondition $Q$.
2. $\{P\wedge \neg b\}S2\{Q\}$: If the precondition $P$ is true and the condition $b$ is false, then executing $S2$ must result in the postcondition $Q$.

Procedure for if Statements:

1. Apply known rules (e.g., the assignment rule) to $S1$ and $S2$ individually. This often involves introducing intermediate assertions.
2. Demonstrate the necessary implications to connect $P$ to the preconditions of the individual branches.

Example 1: Valid Triple

{true} if (x < 0) { y = -x; } else { y = x;} {y ≥ 0}

Breakdown:

if (x < 0) {
  {true ∧ x < 0}  // equivalent to x < 0
  {-x ≥ 0}       // Intermediate assertion
  y = -x;
  {y ≥ 0}
} else {
  {true ∧ ¬(x < 0)} // equivalent to x >= 0
  {x ≥ 0}        // Intermediate assertion
  y = x;
  {y ≥ 0}
}

• Implication 1: $(x<0)⟹(-x\ge 0)$ holds.
• Implication 2: $(x\ge 0)⟹(x\ge 0)$ holds trivially. Therefore, the entire triple is valid.

Example 2: Invalid Triple (Slight change in postcondition)

{true} if (x < 0) { y = -x; } else { y = x;} {y > 0}

Breakdown:

if (x < 0) {
  {true ∧ x < 0}
  {-x > 0}          // Intermediate assertion
  y = -x;
  {y > 0}
} else {
  {true ∧ ¬(x < 0)}
  {x > 0}          // Intermediate assertion
  y = x;
  {y > 0}
}

• Implication 1: $(x<0)⟹(-x>0)$ holds.
• Implication 2: $(x\ge 0)⟹(x>0)$ does not hold (counterexample: $x=0$). Hence, the triple is invalid.

Example 3:

{x > 0} if (a < 5) { y = 1; } else { y = a * x;} {y > 0}

Breakdown:

if (a < 5) {
  {x > 0 ∧ a < 5}
  {1 > 0}          // Intermediate assertion
  y = 1;
  {y > 0}
} else {
  {x > 0 ∧ ¬(a < 5)} // equivalent to x > 0 and a >= 5
  {a * x > 0}       // Intermediate assertion
  y = a * x;
  {y > 0}
}

• Implication 1: $(x>0\wedge a<5)⟹(1>0)$ holds. Note: $P⟹\text{true}$ holds for any $P$.
• Implication 2: $(x>0\wedge a\ge 5)⟹(a\ast x>0)$ holds. Therefore, the entire triple is valid.

Example 4: Without else Branch

{x == y} if (a > 1) { a = a * x; } {a ≠ y}

Can be treated as having an empty else block. Breakdown:

if (a > 1) {
  {x == y ∧ a > 1}
  {a * x ≠ y}       // Intermediate Assertion
  a = a * x;
  {a ≠ y}
} else {
  {x == y ∧ ¬(a > 1)}  // equivalent to x==y and a <= 1
  {a ≠ y}             // Postcondition must hold even if 'if' block isn't executed
}

You would then proceed to prove the implications $(x==y\wedge a>1)⟹(a\ast x\ne y)$ and $(x==y\wedge a\le 1)⟹(a\ne y)$ as in the previous examples. The postcondition must hold regardless of whether the if block is executed.

Loops and Invariants

Reasoning about loops requires a different approach than reasoning about sequential or conditional statements. Loops involve repeated execution of a code block, and we need a way to assert properties that hold true throughout this repetition. This is where loop invariants come in. A loop invariant is a logical assertion that remains true:

• Before the loop begins: It’s established by the initialization code.
• Before each iteration of the loop: It holds true before the loop condition is checked.
• After each iteration of the loop: The loop body must preserve the invariant.
• After the loop terminates: The invariant, combined with the negation of the loop condition (the reason the loop stopped), helps us establish the desired postcondition.

A “useful” invariant is:

1. Strong enough: to imply the desired postcondition (potentially after some transformations if there’s code after the loop).
2. Weak enough: to be established by the initialization code before the loop and to be preserved by the loop body.

A Strategy for Developing Loops with Invariants

1. Conceptualize: Clearly define the loop’s purpose. What problem are you solving? What should be true after the loop completes?

2. Identify a Candidate Invariant: Formulate a candidate invariant. Ask yourself: “What property remains true throughout the loop’s execution, and how does each iteration contribute to the final result?”

3. Construct the Loop Body: Write the loop body, meticulously ensuring that every statement within it preserves the invariant. If the invariant is true before an iteration, it must remain true after the iteration.

4. Determine the Termination Condition: Define the loop’s termination condition. It should be such that, when combined with the invariant, it logically implies the desired postcondition of the loop.

5. Initialize Before the Loop: Write the code that precedes the loop to establish the invariant, ensuring it holds true before the first iteration begins.

This iterative process of refinement—adjusting the invariant, the loop body, and the initialization—is often necessary to arrive at a correct and verifiable loop implementation.

Example: Integer Division

Goal: Compute the integer quotient q for positive integers x and y, where q == x / y (and x, y, and q are int type; $x>0$, $y>0$).

1. Algorithm Idea: Repeated subtraction of y from x, counting the number of subtractions.

2. Candidate Invariant: $q\ast y+r==x$, where r is the remainder, and q is the number of subtractions performed so far.

3. Loop Body (Invariant Preservation):

   {x > 0 ∧ y > 0}
   // Initialization (TBD)
   {inv: q * y + r == x}
   while (/* Condition (TBD) */) {
     r = r - y; // Decrease remainder
     q = q + 1; // Increment quotient
   }
   {q == x / y}

   Each iteration subtracts y from r and increments q, preserving $q\ast y+r==x$.

4. Termination Condition (Implying Postcondition):

   The loop terminates when $r<y$ (we can no longer subtract y without going negative). We want the invariant and the termination condition to imply the postcondition: $(q\ast y+r==x\wedge r<y)⟹(q==x/y)$.

5. Strengthening the Invariant and Initialization:

The implication in step 4 only holds if $0\le r$. Therefore, we strengthen the invariant to: $q\ast y+r==x\wedge 0\le r$. To establish this invariant initially, we set r = x and q = 0.

Final Code:

{x > 0 ∧ y > 0}
r = x;
q = 0;
{inv: q * y + r == x ∧ 0 ≤ r}
while (r >= y) {
  r = r - y;
  q = q + 1;
}
{q == x / y}

Example: Sum of Natural Numbers

Goal: Calculate $s=\text{sum}(1,n)=1+2+\cdots +n$, where $n\ge 0$.

Version 1:

1. Invariant: $s=\text{sum}(1,i)$
2. Initialization: s = 0; i = 0;
3. Loop Condition: i != n
4. Loop Body: s = s + i + 1; i = i + 1;

{n ≥ 0}
s = 0;
i = 0;
{inv: s = sum(1, i)}
while (i != n) {
  s = s + i + 1;
  i = i + 1;
}
{s = sum(1, n)}

Version 2 (Different Loop Counter):

1. Invariant: $s=\text{sum}(1,k-1)$
2. Initialization: s = 0; k = 1;
3. Loop Condition: k != n + 1
4. Loop Body: s = s + k; k = k + 1;

{n ≥ 0}
s = 0;
k = 1;
{inv: s = sum(1, k-1)}
while (k != n + 1) {
  s = s + k;
  k = k + 1;
}
{s = sum(1, n)}

Continue here: 11 Loop Invariants, Classes and Objects, Attributes, Reference Semantics