// Exercise 1: sum of the first n positive integers, 1 + 2 + ... + n.
// Fill in the loop invariant(s); a correct one relates `r` and `i` at every
// iteration, not just `r` on its own. (Stated as `2 * r == n * (n + 1)` to
// avoid integer division.)
proc sumRange(n: Int) returns (r: Int)
  requires n >= 0
  ensures 2 * r == n * (n + 1)
{
  r := 0;
  var i := 0;
  while (i < n)
    invariant true // TODO: replace with a real invariant
  {
    i := i + 1;
    r := r + i;
  }
}