Program Verification Using Dafny

Compositional Verification Principle

Verification of individual methods where postcondition verified once, precondition checked at each call. After calling a method, only its postcondition is assumed; Dafny does not expand callee implementation. Enables modular reasoning.

Method Call Verification

For method call inc(x), Dafny checks that caller's precondition implies callee's precondition. After call, only callee's postcondition is assumed about return values. Implementation details not examined.

Example 1 Verification Result

method inc requires x > 2 ensures y > 3. In Main: x=3 satisfies precondition, so call valid. Postcondition ensures y > 3, which Dafny can verify. Assert y > 3 holds.

Example 2 Verification Result

method inc requires x > 2 ensures y > 3. In Main: x=4 satisfies precondition. Postcondition only guarantees y > 3, not y > 4. Assert y > 4 cannot be verified from postcondition alone.

Max Method Specification

method max(a: array) returns (m: int) requires a.Length > 1 ensures forall i: int :: 0

Max Method Assertion Failure

In Main: a = [0,1,3]. Postcondition ensures y >= each element, but y could be 5, 10, etc. Assert y == 3 cannot be proved because postcondition is too weak.

Max Method Loop Invariant Needed

Loop invariant must track maximum found so far: invariant forall j: int :: 0

Square Method by Sum of Odds

method square(x: nat) returns (y: int) ensures y == x * x. Uses identity: sum of first x odd numbers = x². Loop adds odd numbers: b starts at 1, increments by 2 each iteration.

Square Method Loop Invariant

Invariant: a == i * i and b == 2*i + 1. Initially i=0: a=0, b=1. Each iteration: a += b gives (i² + (2i+1)) = (i+1)², b += 2 gives 2(i+1)+1.

Loop Invariant for Max

invariant forall j: int :: 0

Dafny Assertion Verification

Dafny uses weakest precondition to verify assertions. Assert statement must be provable from current context (preconditions, loop invariants, postconditions of called methods).

Array Element Assignment

a[0] := 0; updates array element. Dafny tracks array contents through modifications. For verification, arrays must be properly initialized before use.

New Array Creation

var a: array := new nat[3]; creates new array of length 3 with unspecified initial values. Elements must be explicitly assigned before reading.

Method Parameter Immutability

In Dafny, method parameters are immutable. To modify values, use returns clause to produce new values. Array contents can be modified via indices.

Loop Invariant Necessity

For loops, Dafny requires invariants to prove properties. Without invariants, Dafny cannot verify that loop establishes required postcondition. Invariants must be inductive (hold before loop, preserved by body).

Termination Proof via Decrease

For loops, Dafny requires decrease clause to prove termination. For simple loops with integer counter, decrease can be automatically inferred. Complex loops need explicit variant