Weakest Precondition Lab — Dijkstra Formal Verification Workbench

1. Formal Hoare Specification {P} S {Q}

Precondition P Initial predicate e.g. n >= 0

Program S (Guarded Commands / Sequential) := ; while do done

Loop Invariant I Maintained across loop iterations

Termination Variant V Integer expression >= 0 strictly decreasing

Postcondition Q Target goal state

Interactive Execution Tracer & Invariant Probe

Parameter n: 25

Iter (k)	r	Guard B	Invariant I	Variant V

Polite calculational logic (Dijkstra EWD-1300): Every mathematical step carries an explicit justification so verification can be checked without pencil and paper.

2. Calculational Proof & Weakest Preconditions All VCs Sound

Computed wp(S, Q)

0 * 0 <= n && (n >= 0)

Verification Conds

4 / 4 Proved

Loop Invariant

Preserved

Termination

Strict Decr V

3. Proof Certificate Export