// summation: return the sum of all values from 1 to n val N:Nat; type number = ℕ[N]; type index = ℕ[N+1]; type result = ℕ[N⋅(1+N)/2]; proc summation(n:number): result requires n ≥ 0; ensures result = ∑j:number with 1 ≤ j ∧ j ≤ n. j; { var s:result ≔ 0; var i:index ≔ 1; while i ≤ n do invariant s = ∑j:number with 1 ≤ j ∧ j ≤ i-1. j; invariant 1 ≤ i ∧ i ≤ n+1; decreases n+1-i; { s ≔ s+i; i ≔ i+1; } return s; } // the verification conditions to be proved // for the total correctness of the program pred Input(n:number, s:result, i:index) ⇔ n ≥ 0 ∧ s = 0 ∧ i = 1; pred Output(n:number, s:result) ⇔ s = ∑j:number with 1 ≤ j ∧ j ≤ n. j; pred Invariant(n:number, s:result, i:index) ⇔ (s = ∑j:number with 1 ≤ j ∧ j ≤ i-1. j) ∧ 1 ≤ i ∧ i ≤ n+1; fun Termination(n:number, s:result, i:index): number = n+1-i; theorem A(n:number, s:result, i:index) ⇔ Input(n, s, i) ⇒ Invariant(n, s, i); theorem T(n:number, s:result, i:index) ⇔ Invariant(n, s, i) ⇒ Termination(n, s, i) ≥ 0; theorem B(n:number, s:result, i:index) ⇔ Invariant(n, s, i) ∧ i ≤ n ⇒ Invariant(n, s+i, i+1) ∧ Termination(n, s+i, i+1) < Termination(n, s, i); theorem C(n:number, s:result, i:index) ⇔ Invariant(n, s, i) ∧ ¬(i ≤ n) ⇒ Output(n, s);