Program Verification Using Dafny

Compositional Verification Principle

• Verification of methods individually

• Postcondition checked after call

• Precondition checked at each call

• Supports modular reasoning.

Method Call Verification

• For call inc(x), checks preconditions

• Caller precondition implies callee's precondition

• Postcondition assumed about return values.

Example 1 Verification Result

• Method inc requires x > 2
• In Main: x=3 satisfies precondition
• Postcondition guarantees y > 3
• Assert y > 3 holds.

Example 2 Verification Result

• Method inc requires x > 2
• In Main: x=4 satisfies precondition
• Postcondition guarantees y > 3, not y > 4
• Assert y > 4 cannot be verified.

Max Method Specification

• Method max(a: array) returns (m: int)
• Requires a.Length > 1
• Ensures m >= a[i] for all valid i.
• Postconditions only ensure upper bound.

Max Method Assertion Failure

• In Main: a = [0,1,3]
• Postcondition y >= each element
• y could be 5, 10; cannot assert y == 3.

Max Method Loop Invariant Needed

• Track maximum: invariant m >= a[j]
• Ensure m is actual maximum, not just upper bound.

Square Method by Sum of Odds

• Method square(x: nat) returns (y: int)
• Ensures y == x * x
• Uses sum of first x odd numbers.

Square Method Loop Invariant

• Invariant: a == i * i, b == 2*i + 1
• Initially: i=0, a=0, b=1
• Each iteration updates a and b.

Loop Invariant for Max

• Invariant m >= a[j] for all j < i
• Also need invariant m == a[j] to ensure m is maximum.

Dafny Assertion Verification

• Uses weakest precondition for assertions
• Assert must be provable from context.

Array Element Assignment

• a[0] := 0 updates element
• Tracks array contents for verification.

New Array Creation

• var a: array := new nat[3];
• Creates new array of length 3
• Elements must be assigned before reading.

Method Parameter Immutability

• Parameters are immutable in Dafny
• Use returns clause for new values.

Loop Invariant Necessity

• Invariants required for proving properties
• Must hold before and be preserved by loop body.

Termination Proof via Decrease

• Requires decrease clause for termination proof
• Simple loops can infer decrease automatically.