// MIT 6.S057 Fall 2026, Class 1

// Some fancier examples to show off the power and basic ideas of Dafny

// Three ways to write one simple function:
// look up whether an integer is present in an "array" of integers,
// returning the position if so.
// Note that earlier classes have harped on the importance of comments
// to explain the purposes of functions, but here we write that information
// out formally instead!

// This version uses two 'ensures' clauses with different implications.
method IndexOf_recursive_two_implications(s: seq<int>, e: int) returns (res: int)
  requires 0 < |s|
  ensures res < 0 ==> e !in s
  ensures 0 <= res ==> res < |s| && s[res] == e
{
  if s[0] == e {
   res := 0;
  } else {
    if |s| == 1 {
      res := -1;
    } else {
      res := IndexOf_recursive_two_implications(s[1..], e);
      if res != -1 {
        res := res + 1;
      }
    }
  }
}

// This version instead uses one 'ensures' with an 'or'.
// Can you spot a practical difference between these two specificatons?
method IndexOf_recursive_disjunction(s: seq<int>, e: int) returns (res: int)
  requires 0 < |s|
  ensures (res == -1 && e !in s) || (0 <= res < |s| && s[res] == e)
{
  if s[0] == e {
   res := 0;
  } else {
    if |s| == 1 {
      res := -1;
    } else {
      res := IndexOf_recursive_disjunction(s[1..], e);
      if res != -1 {
        res := res + 1;
      }
    }
  }
}

// We can also write this routine with a loop, though it forces us to
// add a loop invariant.
method IndexOf_iterative(s: seq<int>, e: int) returns (res: int)
  requires 0 < |s|
  ensures res < 0 ==> e !in s
  ensures 0 <= res ==> res < |s| && s[res] == e
{
  for i := 0 to |s|
    invariant e !in s[..i] {
    if s[i] == e {
      return i;
    }
  }

  return -1;
}

// Here is another classic: insertion sort!
// Note that 'seq' above is for an immutable "array," whereas here we go mutable.

method InsertionSort(a: array<int>)
  modifies a
  ensures multiset(a[..]) == old(multiset(a[..]))
  ensures forall n, m :: 0 <= n < m < a.Length ==> a[n] <= a[m]
{
  for i := 0 to a.Length
    invariant multiset(a[..]) == old(multiset(a[..]))
    invariant forall n, m :: 0 <= n < m < i ==> a[n] <= a[m]
    invariant forall n, m :: 0 <= n < i <= m < a.Length ==> a[n] <= a[m]
  {
    var lowest := i;

    for j := i+1 to a.Length
      invariant i <= lowest < j
      invariant forall k :: i <= k < j ==> a[lowest] <= a[k]
      // invariant multiset(a[..]) == old(multiset(a[..]))
      // invariant forall n, m :: 0 <= n < m < i ==> a[n] <= a[m]
      // invariant forall n, m :: 0 <= n < i && i <= m < a.Length ==> a[n] <= a[m]
      // One might have expected the above three invariants to be required,
      // but Dafny is smart about noticing that this loop does not *modify*
      // the array 'a', hence prior knowledge about 'a' is preserved.
    {
      if a[j] < a[lowest] {
        lowest := j;
      }
    }

    var old_i := a[i];
    a[i] := a[lowest];
    a[lowest] := old_i;
  }
}

// Now let's go back through the basics.
// We include multiple numbered versions, to capture different edits made in class.

method Triple(x: int) returns (r: int) {
  var y := 2 * x;
  r := x + y;
  assert r == 3 * x;
}

method Triple2(x: int) returns (r: int) {
  var y := 2 * x;
  r := x + y;
  assert r == 10 * x;
  assert r < 5; // Very surprising this one is accepted by Dafny!  Do you see why?
  assert false;
}

method Triple3(x: int) returns (r: int) {
  if x == 0 {
    r := 0;
  } else {
    var y := 2 * x;
    r := x + y;
  }
  assert r == 3 * x;
}

method Caller() {
  var t := Triple(18);
  assert t < 100;
}

method Triple4(x: int) returns (r: int)
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
}

method Caller2() {
  var t := Triple4(18);
  assert t < 100;
}

method Triple5(x: int) returns (r: int)
  requires x % 2 == 0
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
}

method Index(n: int) returns (i: int)
  requires 1 <= n
  ensures 0 <= i < n
{
  i := n / 2;
}

method Index2(n: int) returns (i: int)
  requires 1 <= n
  ensures 0 <= i < n
{
  i := 0;
}

method Doesn'tWork() {
  var x := Index(50);
  var y := Index(50);
  assert x == y;
}

method Min0(x: int, y: int) returns (m: int)
  ensures m <= x && m <= y

method Min(x: int, y: int) returns (m: int)
  ensures m <= x && m <= y
  ensures m == x || m == y

function Average(a: int, b: int): int {
  (a + b) / 2
}

method Triple'(x: int) returns (r: int)
  ensures Average(r, 3 * x) == 3 * x

function Average2(a: int, b: int): int
  requires 0 <= a && 0 <= b
{
  (a + b) / 2
}

method Triple6(x: int) returns (r: int)
  ensures r == 3 * x
{
  if 0 <= x {
    r := Average(2 * x, 4 * x);
  } else {
    r := -Average(-2 * x, -4 * x);
  }
}

method IllegalAssignment() returns (y: int) {
  ghost var x := 10;
  y := 2 * x;
}

ghost method DoubleQuadruple(x: int) returns (a: int, b: int)
  ensures a == 2 && b == 4 * x
{
  a := 2 * x;
  b := 2 * a;
}

method Triple7(x: int) returns (r: int)
  ensures r == 3 * x
{
  var y := 2 * x;
  r := x + y;
  ghost var a, b := DoubleQuadruple(x);
  assert a <= r <= b || b <= r <= a;
}