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
.
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:
2. Backward Reasoning (GoalOriented 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:
Comparison
Feature  Forward Reasoning  Backward Reasoning 

Direction  Follows program flow  Reverse program flow 
Focus  Deriving consequences  Finding necessary conditions 
Assertions  Can become complex  More concise 
Usefulness  Exploring program behavior  Verifying specific properties 
Assignment Rules
For assignment statements, the Hoare triple takes the following form:
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:
 Replace all occurrences of $X$ in $Q$ with $E$, resulting in $Q_{′}$.
 Demonstrate that the implication $P⟹Q_{′}$ holds. In other words, if $P$ is true, then $Q_{′}$ must also be true.
Rationale:
Let’s break down why this rule works:
 We want to ensure that the postcondition $Q$ is true after the assignment $X=E$.
 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_{′}$) must have been true before the assignment.
 By showing that $P⟹Q_{′}$, we are demonstrating that $P$ is a sufficiently strong precondition to guarantee that $Q_{′}$ 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:
To establish the validity of the combined segment:
We must fulfill two conditions:
 Prove the validity of each individual triple:
{P1} S1 {Q1}
and{P2} S2 {Q2}
.  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):
We decompose this into two separate triples:

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.

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

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:
 $A1$ has a stronger precondition than $A2$ because $(a>0∧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:
Or, equivalently:
This triple is valid if and only if both of the following triples are valid:
 ${P∧b}S1{Q}$: If the precondition $P$ and the condition $b$ are true, then executing $S1$ must result in the postcondition $Q$.
 ${P∧¬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:
 Apply known rules (e.g., the assignment rule) to $S1$ and $S2$ individually. This often involves introducing intermediate assertions.
 Demonstrate the necessary implications to connect $P$ to the preconditions of the individual branches.
Example 1: Valid Triple
Breakdown:
 Implication 1: $(x<0)⟹(−x≥0)$ holds.
 Implication 2: $(x≥0)⟹(x≥0)$ holds trivially. Therefore, the entire triple is valid.
Example 2: Invalid Triple (Slight change in postcondition)
Breakdown:
 Implication 1: $(x<0)⟹(−x>0)$ holds.
 Implication 2: $(x≥0)⟹(x>0)$ does not hold (counterexample: $x=0$). Hence, the triple is invalid.
Example 3:
Breakdown:
 Implication 1: $(x>0∧a<5)⟹(1>0)$ holds. Note: $P⟹true$ holds for any $P$.
 Implication 2: $(x>0∧a≥5)⟹(a∗x>0)$ holds. Therefore, the entire triple is valid.
Example 4: Without else
Branch
Can be treated as having an empty else
block. Breakdown:
You would then proceed to prove the implications $(x==y∧a>1)⟹(a∗x=y)$ and $(x==y∧a≤1)⟹(a=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.
Challenges of Loop Invariants:
 Discovery: Finding a suitable loop invariant is not a mechanical process; it often requires insight into the algorithm’s logic. There’s no single “correct” invariant; multiple invariants might work for the same loop, each offering a different perspective on its behavior.
 Balance: A good invariant strikes a balance between being strong enough to prove the desired postcondition and weak enough to be easily established and maintained by the loop.
 Iteration: You might need to refine your invariant as you develop the loop, adjusting it to fit the evolving logic of your code.
A Strategy for Developing Loops with Invariants

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

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?”

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.

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.

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$).

Algorithm Idea: Repeated subtraction of
y
fromx
, counting the number of subtractions. 
Candidate Invariant: $q∗y+r==x$, where
r
is the remainder, andq
is the number of subtractions performed so far. 
Loop Body (Invariant Preservation):
Each iteration subtracts y
from r
and increments q
, preserving $q∗y+r==x$.
 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∗y+r==x∧r<y)⟹(q==x/y)$.
 Strengthening the Invariant and Initialization:
The implication in step 4 only holds if $0≤r$. Therefore, we strengthen the invariant to: $q∗y+r==x∧0≤r$. To establish this invariant initially, we set r = x
and q = 0
.
Final Code:
Example: Sum of Natural Numbers
Goal: Calculate $s=sum(1,n)=1+2+⋯+n$, where $n≥0$.
Version 1:
 Invariant: $s=sum(1,i)$
 Initialization:
s = 0; i = 0;
 Loop Condition:
i != n
 Loop Body:
s = s + i + 1; i = i + 1;
Version 2 (Different Loop Counter):
 Invariant: $s=sum(1,k−1)$
 Initialization:
s = 0; k = 1;
 Loop Condition:
k != n + 1
 Loop Body:
s = s + k; k = k + 1;