// summation: return the sum of all values from 1 to n

val N:ℕ;
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) 
  requires n ≥ 0;
⇔ Input(n, s, i) ⇒ Invariant(n, s, i);
  
theorem T(n:number, s:result, i:index) 
   requires n ≥ 0;
⇔ Invariant(n, s, i) ⇒ Termination(n, s, i) ≥ 0;

theorem B(n:number, s:result, i:index) 
  requires n ≥ 0;
⇔ 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) 
  requires n ≥ 0;
⇔ Invariant(n, s, i) ∧ ¬(i ≤ n) ⇒ Output(n, s);



