method Divide(a: int, b: int) returns (r: int)
  requires b != 0
  ensures r == a / b
{
  return a / b;
}

method DivideCaller(x: int)
{
  var t := Divide(100, 2 * x + 1);
  assert t <= 100;
}

method DivideCaller_model(x: int)
{
  var a', b' := 100, 2 * x + 1;
  // TODO assert something (why?)

  var r': int;
  // TODO assume something (why?)
  // (Dafny will give you an error and a warning about the assumption.)

  var t := r';
  assert t <= 100;
}

method DivideCaller_forward(x: int)
{
  var a', b' := 100, 2 * x + 1;
  assert a' == 100 && b' == 2 * x + 1; // (1) <- we start here

  // TODO assert something (copy from above)
  // (The assertion needs to hold given what we knew. We don't learn anything.)
  assert a' == 100 && b' == 2 * x + 1; // (2) <- no change

  var r': int;
  // TODO assume something (copy from above)
  assert true; // (3)

  var t := r';
  assert true; // (4)

  assert t <= 100;
}

method DivideCaller_backward(x: int)
{
  assert true; // (6)
  var a', b' := 100, 2 * x + 1;

  assert true; // (5)
  // TODO assert something (copy from above)

  assert true; // (4)
  var r': int;

  assert true; // (3)
  // TODO assume something (copy from above)

  assert r' <= 100; // (2)
  var t := r';

  assert t <= 100; // (1) <- remember to start here!
}