// given natural numbers n and m, we want to compute // the quotient q and remainder r of n divided by m // the type of natural numbers less than equal N val N: ℕ; type Num = ℕ[N]; // the precondition of the computation pred pre(n:Num, m:Num) ⇔ m ≠ 0; // the postcondition, first formulation pred post1(n:Num, m:Num, q:Num, r:Num) ⇔ n = m⋅q + r ∧ ∀q0:Num, r0:Num. (n = m⋅q0 + r0 ⇒ r ≤ r0); // the postcondition, second formulation pred post2(n:Num, m:Num, q:Num, r:Num) ⇔ n = m⋅q + r ∧ r < m; // for all inputs that satisfy the precondition // both formulations are equivalent: // ∀n:Num, m:Num, q:Num, r:Num. // pre(n, m) ⇒ (post1(n, m, q, r) ⇔ post2(n, m, q, r)); theorem postEquiv(n:Num, m:Num, q:Num, r:Num) requires pre(n, m); ⇔ post1(n, m, q, r) ⇔ post2(n, m, q, r); // we will thus use the simpler formulation from now on pred post(n:Num, m:Num, q:Num, r:Num) ⇔ post2(n, m, q, r); // 1. investigate whether the specified // input/output combinations are as desired fun quotremFun(n:Num, m:Num): Tuple[Num,Num] requires pre(n, m); ensures post(n, m, result.1, result.2); = choose q:Num, r:Num with post(n, m, q, r); // 2. check that some but not all inputs are allowed theorem someInput() ⇔ ∃n:Num, m:Num. pre(n, m); theorem notEveryInput() ⇔ ∃n:Num, m:Num. ¬pre(n, m); // 3. check that for all inputs that satisfy the precondition // there are some outputs that satisfy the postcondition theorem someOutput(n:Num, m:Num) requires pre(n, m); ⇔ ∃q:Num, r:Num. post(n, m, q, r); // 4. check that not every output satisfies the postcondition theorem notEveryOutput(n:Num, m:Num) requires pre(n, m); ⇔ ∃q:Num, r:Num. ¬post(n, m, q, r); // 5. check that the output is uniquely defined // (optional, need not generally be the case) theorem uniqueOutput(n:Num, m:Num) requires pre(n, m); ⇔ ∀q:Num, r:Num. post(n, m, q, r) ⇒ ∀q0:Num, r0:Num. post(n, m, q0, r0) ⇒ q = q0 ∧ r = r0; // 6. check whether the algorithm satisfies the specification proc quotRemProc(n:Num, m:Num): Tuple[Num,Num] requires pre(n, m); ensures post(n, m, result.1, result.2); { var q: Num = 0; var r: Num = n; while r ≥ m do // invariant and termination measure for verification invariant n = q⋅m + r; decreases r; { r ≔ r-m; q ≔ q+1; } return ⟨q,r⟩; }