// SE 504 Spring 2026
// HW #3
// Name: ...


// RWM: Here is the annotated solution to Exercise 2.18 in the
//      Program Proofs textbook

method Exercise_2_18(x: int) returns (y: int)
  requires x == 50   // (5.2)  (wp of method body wrt postcondition)
  ensures x + y == 100
{
  assert x == 50;   // 5.2 simplifies (5.1)
  assert x >= 3  && (x >= 3 ==> x == 50);  //  5.1 (simplifies both conjuncts of (5))
  assert (x < 3 ==> x == 89) && (!(x < 3) ==> x == 50);  // 5 (wp from if-else below)
  if x < 3 {
    assert x == 89;          // 3.1 (simplifies (3))
    assert x+1 + 10 == 100;  // 3 (wp from (1))
    var x,y := x+1, 10;
    assert x+y == 100;   // 1 (postcondition)
  } 
  else {
    assert x == 50;      // 4.1 (simplifies (4))
    assert x+x == 100;   // 4  (wp from (2))
    y := x;
    assert x+y == 100;   // 2 (postcondition)
  }
  assert x+y == 100; 
}


// Problem 1:
// ----------

method Exercise_2_20(x: int) returns (y: int)
  requires true  // placeholder
  ensures x + y == 22
{
  if x < 20 {
    y := 3;
  }
  else {
    y := 2;
  }
  assert x + y == 22;
}


// Problem 2:
// ----------

method Exercise_2_21(x: int) returns (y: int)
  requires true  // placeholder
  ensures y < 10
{
  if x < 8 {
    if x == 5 {
      y := 10;
    }
    else {
      y := 2;
    }
  }
  else {
    y := 0;
  }
  assert y < 10;
}


// Problem 3:
// ----------

method Exercise_2_22(x: int) returns (y: int)
  requires true  // placeholder
  ensures y % 2 == 0
{
  if x < 10 {
    if x < 20 {
      y := 1;
    }
    else {
      y := 2;
    }
  }
  else {
    y := 4;
  }
  assert y % 2 == 0;
}


// Problem 4:
// ----------

method Exercise_2_23(X: int, Y: int) returns (y: int)
  requires true  // placeholder
  ensures y % 2 == 0
{
  var x := X;
  y := Y;
  if x < 8 {
    if x < 4 {
      x := x+1;   // replaced x on LHS with y
    }
    else {
      y := 2;
    }
  }
  else {  // x >= 8
    if x < 32 {
      y := 1;
    }
    else {
      // do nothing
    }
  }
  assert y % 2 == 0;
}


// Problem 5:
// ----------

method Exercise2_24(x: int) returns (y: int)
  requires true  // placeholder
  ensures 0 <= y < 100
{
  if x < 34 {
    if x == 2 {
      y := x+1;
    }
    else {
      y := 233;
    }
  }
  else {
    if x < 55 {
      y := 21;
    }
    else {
      y:= 144;
    }
  } 
  assert 0 <= y < 100;
}


// Problem 6:
// ----------

method Multiply(X: int, Y: int) returns (x: int, y: int, z: int)
  requires true   // placeholder
  ensures X*Y == x*y + z
{
  x,y := X,Y;
  z := 0;
  if x == 0 {
    // do nothing
  }
  else {
    if (x % 2 == 0) {
      x := x / 2;
      y := y + y;
    }
    else {
      x,z := x-1, z+y;
    }
  }
  assert X*Y == x*y + z;
}