method Foo() returns (x : int)
  requires true
  ensures (x == 84)
{ 
  // {{ true }} ->> (1)
  // {{ P[n|->0][i|->0] }}
  var i := 0;
  // {{ P[n|->0] }}
  var n := 0; 
  // {{ P }}
  while (i < 42)
    invariant (n == 2*i && i <= 42)
  {
    // {{ P /\ (i < 42) }} ->> (2)
    // {{ P[n |-> n + 2][i |-> i+1 ] }}
    i := i + 1;
    // {{ P[n |-> n + 2] }}
    n := n + 2;
    // {{ P }}
  }
  // {{ P /\ !(i < 42) }} ->> (3)
  // {{ n == 84 }}
  x := n;
  // {{ x == 84 }}
}

/* Invariant P needs to satisfy 3 conditions:
   (1) {{ true }} ->> {{ P[n|->0][i|->0] }}
   (2) {{ P /\ (i < 42) }} ->> {{ P[n |-> n + 2][i |-> i+1 ] }}
   (3) {{ P /\ !(i < 42) }} ->> {{ n == 84 }}

   P := n == 2 * i /\ i <= 42 
   (1)   {{ true }} ->> {{ 0 = 0 /\ <= 42 }}
   (2)   {{ n = 2 * i /\ i <= 42 /\ (i < 42) }} ->> {{ n + 2 = 2 * (i + 1) /\ (i+1) <= 42}}
   (3)   {{ n == 2 * i (i <= 42) /\ !(i < 42) }} ->> {{ n == 84 }}

*/