method ExampleMethod(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  var a, b;

  a := x + 3;
  if x < 20 {
    b := 32 - x;
  } else {
    b := 16;
  }

  y := a + b;
}



method ExampleMethod_forward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  // (1) what do we already know?
  assert true;

  var a, b;

  // we don't learn anything from declaring those variables

  a := x + 3;

  // (2) use && to create a formula that records what we knew and what we know:
  assert true;

  // time to reason through an `if`...
  if x < 20 {
    // (3a) if we got here, what do we know?
    assert true;

    b := 32 - x;

    // (4):
    assert true;
  } else {
    // (3b) if we got here, what do we know?
    assert true;

    b := 16;

    // (5):
    assert true;
  }

  // (6) combine formulas (4) and (5)... how?
  assert true;

  y := a + b;

  // (7):
  assert true;

  // (8) we need that formula to imply the postcondition:
  assert true;
}



method ExampleMethod_backward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  // (8) we need the precondition to imply that formula:
  assert true;

  var a, b;

  // (7):
  assert true;

  a := x + 3;

  // (6) mechanically combine (4), (5), and the guard of the `if` (also use its negation):
  assert true;

  if x < 20 {
    // (5):
    assert true;

    b := 32 - x;

    // (3b) what needs to be true here?
    assert true;
  } else {
    // (4):
    assert true;

    b := 16;

    // (3a) what needs to be true here?
    assert true;
  }
  // time to reason back through an `if`...

  // (2) before assignment, we need:
  assert 25 <= a + b;

  y := a + b;

  // (1) start with the postcondition:
  assert 25 <= y;
}