3  Blatt 03

Problem 1

We use a slightly different, more convenient method based on Hoare calculus and the program derivation methodoloy of Dijkstra. In this methodology pre- and postconditions, as well as loop invariants are provided directly within the program text as comments.

A commment before a command is a logical statement about the state-space of the program before the execution of the command, i.e. the precondition, and the comment after is the postcondition.

The comment before a while or a for loop is specifically labeled as ‘invariant’ and is the invariant statement that stays true after the execution of the loop. The general form of such specification is:

# P
C
# Q

This expression means: if P holds before the execution of C then Q will hold after the execution of C. For example:

# x == 0
x += 1
# x == 1

or

# y > 0
y -= 1
# y >= 0

or

# x == X and y == Y
x += y
# x == X + Y and y == Y
y = x - y
# x == X + Y and Y == X
x -= y
# x == X and Y == X

or more compactly

# x == X and y == Y
x += y
y =  x - y
x = x - y
# x == Y and y == X

In the above program we exchnaged the values of variables x, and y without using a temporary varible t. But as a furhter example of pre- and postcondition specification let’s do that:

# x == X and y == Y
t = x
# t == X
x = y
# x == Y
y = t
# y == X

The semantics of while loops is given as follows:

if

# P and Q
C
# P

Where C is an arbitrary command, or a sequence of commands.

Then:

# invariant: P
while Q :
    C
# P and !Q

So what we have to show is that:

  1. P holds before the execution of the loop, before C is executed (induction base)
  2. if Q holds additionally then P still holds after C is executed (inductive step)

Having shown 1) and 2) we can conclude:

  1. After exiting the loop (P and !Q) holds

A simple example: incrementing a variable i up to a value N, where it is assumed that N >= 0

i = 0
# invariant: i <= N (since we know that 0 <= N)
while i < N:
    i += 1
# i >= N
  1. IB: Before the loop executes: i == 0 <= N, by assumption.
  2. IS: if i <= N and i < N simply implies i < N. if i < N holds before incrementation, then i <= N will hold after the incrementation, by simple arithmetic rules, which proves the invariant.

So, after exiting the loop the following holds:

  1. i <= N and !(i < N). which is exactly equivalent to i == N, what

Let’s apply this scheme to the division example:

def div(x, y):
    # precondition: x >= 0, y > 0
    q = 0 
    r = x
    # invariant: x == r + q * y and r >= 0
    while r >= y:
        r -= y
        q += 1
    # r < y 
    return (q, r)

print(f"31/9 == {div(31, 9)[1]} + 9 * {div(31,9)[0]}")
31/9 == 4 + 9 * 3

Proof:

  1. IB: before the loop executes we have; q == 0 and 0 <= x == r therefore x == r + q * y and r >= 0 holds trivially.

  2. IS: assume the invariant holds before some arbitrary execution of the loop. Assume that r >= y additionally holds, so we are in the body of the loop. Now since the invariant holds we have

    x == r + q * y and r >= 0 and r >= y

    we can manipulate r + q * y as follows:

    r + q * y == (r - y) + (q + 1) * y

    So after executing the body of the loop the r holds what previously was r - y and q holds what previously was q + 1. But as shown above this leaves the value of expression unchanged, therefore after updating the variables r and q in the body of the loop the equality x == r + q * y still holds.

    Now we turn our attention to the second conjunct of the invariant: r >= 0. Since r >= y holds in the body of the loop, r >= 0 still holds after the update to r - r -= y.

    These two observations conclude our proof

Now after exiting the loop in addition to the invariant the negation of the loop condition holds. Thus we have:

  1. x == r + q * r and r >= 0 and !(r >= y) iff x == r + q * r and 0 <= r < y

Which is exactly satisfies the condition of whole number division.

Below we give the trace of the execution of the algorith for x == 31 and y == 9 with a short explanation of Hoare-style secification:

Hoare Logic Specification for Integer Division

Problem: Implement integer division with remainder using repeated subtraction.

Function:

def div(x, y):
    # Precondition: x ≥ 0 ∧ y > 0
    q = 0
    r = x
    # Invariant: x == r + q * y ∧ r ≥ 0
    while r >= y:
        r = r - y
        q = q + 1
    # Postcondition: x == q * y + r ∧ 0 ≤ r < y
    return (q, r)

Hoare Triple:

\[ \{\, x \geq 0 \wedge y > 0 \,\} \\ \texttt{div(x, y)} \\ \{\, x = q \cdot y + r \wedge 0 \leq r < y \,\} \]

  • Invariant: \(x = r + q \cdot y \quad \wedge \quad r \geq 0\)
  • Termination: Each iteration decreases r by y while keeping r ≥ 0 therefore the loop will eventually terminate.

Execution Trace: div(31, 9)

Initial values: x = 31, y = 9

q r Invariant: r + y * q == x ∧ r ≥ 0 Loop condition (r ≥ y)
0 31 31 + 9 * 0 = 31 ∧ 31 ≥ 0 → true 31 ≥ 9 → true
1 22 22 + 9 * 1 = 31 ∧ 22 ≥ 0 → true 22 ≥ 9 → true
2 13 13 + 9 * 2 = 31 ∧ 13 ≥ 0 → true 13 ≥ 9 → true
3 4 4 + 9 * 3 = 31 ∧ 4 ≥ 0 → true 4 ≥ 9 → false
  • The loop terminates when r < y, here r = 4 < 9.
  • Final return: (q, r) = (3, 4)
  • Confirming: \(31 = 9 \cdot 3 + 4\)

This demonstrates partial correctness (postcondition holds if it terminates), and the termination argument ensures total correctness.