// Here is an innocuous method that meets a simple specification.
// How does Dafny check that the method is correct?
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;
}

// Let's trace through _what Dafny knows_ at each line, by using
// assertions.
method ExampleMethod_forward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  // Well, to start with, we know the precondition.
  assert 10 <= x;

  var a, b;
  // We don't learn anything going through this variable declaration.
  // The variables could store anything!

  a := x + 3;
  assert 10 <= x && a == x + 3;
  // We use "and" to record that we learned the value of 'a'.

  if x < 20 {
    // Important: here we know that the 'if' test succeeded!
    assert 10 <= x && a == x + 3 && x < 20;
    b := 32 - x;
    assert 10 <= x && a == x + 3 && x < 20 && b == 32 - x;
  } else {
    // Now we know that the test _failed_.
    assert 10 <= x && a == x + 3 && !(x < 20);
    b := 16;
    assert 10 <= x && a == x + 3 && !(x < 20) && b == 16;
  }

  // What's true true after the 'if'?
  // We must have followed one of the two paths, which is well-expressed with 'or'.
  assert (10 <= x && a == x + 3 && x < 20 && b == 32 - x)
      || (10 <= x && a == x + 3 && !(x < 20) && b == 16);

  y := a + b;
  assert ((10 <= x && a == x + 3 && x < 20 && b == 32 - x)
          || (10 <= x && a == x + 3 && !(x < 20) && b == 16))
      && (y == a + b);

  // At this point, we simply check that the formula we calculated implies the
  // method postcondition!  That check can be phrased as a formula itself:
  assert (((10 <= x && a == x + 3 && x < 20 && b == 32 - x)
            || (10 <= x && a == x + 3 && !(x < 20) && b == 16))
          && (y == a + b)) ==> 25 <= y;

  // We could check whether the postcondition would also hold in alternative
  // scenarios.
  assert (((10 <= x && a == x + 3 && x < 21 && b == 999 - x)
    || (10 <= x && a == x + 3 && !(x < 21) && b == 13))
    && y == a + b) ==> 25 <= y;
  // Do note that this implication is checked given our knowledge of what could
  // be true at this point in the program.  If the formula to the left of the
  // implication _contradicts_ what we know, then the implication holds trivially!
}

// There was a gotcha lurking in our intuitive method of modeling the effect of
// an assignment statement.  How does it work for this program?
method Swap(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  a, b := x, y;
  assert a == x && b == y;

  var tmp := a;
  assert a == x && b == y && tmp == a;
  // OK, the next one is going to be trouble.
  a := b;
  // assert a == x && b == y && tmp == a && a == b;
  // Nope, can't prove that one!
  b := tmp;
}

// When variables are being reassigned as a method proceeds, our naive forward
// calculation of predicates gives the wrong results.  Instead,
// counterintuitively, we can calculate _backward_!
// Please read the assertion annotations here from the end of the method to the
// beginning.
method Swap_backward(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  // Excellent!  The final formula we calculate is obviously true, which is
  // necessary, since we have no precondition/'requires'.
  
  // This rule easily generalizes to parallel assignment (multiple variables to
  // left of ':=').
  assert y == y && x == x;
  a, b := x, y;

  assert b == y && a == x;
  var tmp := a;

  assert b == y && tmp == x;
  a := b;

  // The rule for assignment may now be surprising: _replace_ all mentions of
  // the variable being assigned, turning them into copies of the expression
  // being assigned!
  assert a == y && tmp == x;
  b := tmp;

  // Our easy starting point: copy in the postcondition.
  assert a == y && b == x;
}

// Let's repeat the backward exercise for our initial example.
method ExampleMethod_backward(x: int) returns (y: int)
  requires 10 <= x
  ensures 25 <= y
{
  // We need to confirm that our precondition truly implies that formula,
  // which proof goal we restate here explicitly.
  assert 10 <= x ==> ((x < 20 && 25 <= (x + 3) + (32 - x)) || (!(x < 20) && 25 <= (x + 3) + 16));

  var a, b;

  assert (x < 20 && 25 <= (x + 3) + (32 - x)) || (!(x < 20) && 25 <= (x + 3) + 16);
  a := x + 3;

  // Now we mechanically create an "or" of the two top formulas of the blocks,
  // also "and"ing in the 'if' expression or its negation.
  assert (x < 20 && 25 <= a + (32 - x)) || (!(x < 20) && 25 <= a + 16);
  if x < 20 {
    assert 25 <= a + (32 - x);
    b := 32 - x;
    assert 25 <= a + b;
  } else {
    assert 25 <= a + 16;
    b := 16;
    assert 25 <= a + b;
  }
  // Ooo, an 'if'.  What do we do?  Start by copying the current formula into
  // the ends of the two blocks.

  assert 25 <= a + b;
  y := a + b;

  // Easy start: copy in the postcondition.
  assert 25 <= y;
}

// It turns out there _is_ actually a complete rule we can use to calculate
// formulas in the forward direction!  In the case of assignment, we have to
// use an 'exists' quantifier.  Here, then, is how we calculate forwards for our
// swapping method.
method Swap_forward(x: int, y: int) returns (a: int, b: int)
  ensures a == y && b == x
{
  a, b := x, y;
  assert a == x && b == y;

  var tmp := a;
  assert a == x && b == y && tmp == a;
  // We trigger a different, more-complex rule when we _reassign_ a variable vs.
  // assigning it in the first place.
  a := b;
  assert (exists old_a :: old_a == x && b == y && tmp == old_a) && a == b;
  // See how we copied the previous formula, replacing 'a' with a fresh 'old_a'
  // that we assert exists within the new formula?
  // This version is more of a mouthful!  Dafny also raises a warning about not
  // being confident that it fully understands how to take advantage of this
  // quantifier.  Indeed, quantifiers tend to trigger less predictable behavior
  // in the automatic program checker, so that's a pretty good reason to prefer
  // the backwards style.  But let's finish this example anyway.

  b := tmp;
  assert (exists old_b :: (exists old_a :: old_a == x && old_b == y && tmp == old_a) && a == old_b) && b == tmp;

  // Then we can run the final implication check:
  assert ((exists old_b :: (exists old_a :: old_a == x && old_b == y && tmp == old_a) && a == old_b) && b == tmp)
          ==> (a == y && b == x);

  // By the way, these forward-direction calculation rules compute what are known
  // as _strongest postconditions_.  Here, "strongest" means "most precise."  It
  // is always logically sound to be a little less precise, allowing additional
  // program states.  If we let our imaginations run wild and add too many
  // additional possibilities, we will often find ourselves unable to prove
  // postconditions!  However, it's often helpful to apply algebraic
  // simplifications and general beautification.  Here's one alternative to the
  // formula we found with two quantifiers, just noticing that each quantified
  // variable winds up known to be equal to another variable.
  assert tmp == x && a == y && b == tmp;

  // Actually, the method's postcondition is another formula we could choose
  // to simplify to at this point, even independently of proving the method
  // correct!
}

// See Chapter 2 of "Program Proofs" for a more formal take on all of these matters.
// For instance, it presents the dual concept of weakest preconditions.
// Instead of going into those formalities, let's meet some of the useful
// built-in, _immutable_ container types of Dafny, which turn out to work very
// well with this calculational style, because we are allowed to mention
// containers and operations on them in formulas.

// Here's a simple use of sequences, immutable arrays/lists.
// We will annotate all these examples with formulas in the backwards style
// (so again start from the end of the method).
method Sequence1(a: int, b: int) returns (r: int)
  ensures r == a + b
{
  // Great: we're down to a simple arithmetic formula that is easy to check.
  assert 0 <= 0 < 3 && 0 <= 2 < 3 && 0 <= 1 < 3 && a + 3 * b - 2 * b == a + b;
  // That last assertion can be simplified using algebraic properties of
  // sequence operations, to the above:
  assert 0 <= 0 < |[a, 2 * b, 3 * b]| && 0 <= 2 < |[a, 2 * b, 3 * b]| && 0 <= 1 < |[a, 2 * b, 3 * b]| && [a, 2 * b, 3 * b][0] + [a, 2 * b, 3 * b][2] - [a, 2 * b, 3 * b][1] == a + b;
  var s : seq<int> := [a, 2 * b, 3 * b];
  assert 0 <= 0 < |s| && 0 <= 2 < |s| && 0 <= 1 < |s| && s[0] + s[2] - s[1] == a + b;
  r := s[0];
  assert 0 <= 2 < |s| && 0 <= 1 < |s| && r + s[2] - s[1] == a + b;
  r := r + s[2];
  // Note that we add a requirement of in-bounds access, in processing a read
  // from a sequence.
  assert 0 <= 1 < |s| && r - s[1] == a + b;
  r := r - s[1];
  assert r == a + b;
}

// Here is another example, using _slicing_ and _functional update_.
// Each kind of operation builds a _new_ "modified" sequence, since sequences
// are immutable.
method Sequence2(s: seq<int>, i: int) returns (r: seq<int>)
  requires 0 <= i < |s|
  ensures r == s
{
  // This top assertion trivially simplifies into the precondition.  Done!
  assert 0 <= i < |s| && s == s;
  // Going from the line below to the one above, we use the fact that
  // concatenating these two particular slices rebuilds the original sequence.
  assert 0 <= i < |s[..i] + s[i..]| && s[..i] + s[i..] == s;
  r := s[..i] + s[i..];
  assert 0 <= i < |r| && r == s;
  assert 0 <= i < |r| && 0 <= i < |r| && r[i := r[i] + 10 - 10] == s;
  // OK, that last formula is getting unwieldy!  Let's do two rounds of simplification.
  assert 0 <= i < |r| && 0 <= i < |r[i := r[i] + 10]| && r[i := r[i] + 10][i := r[i := r[i] + 10][i] - 10] == s;
  r := r[i := r[i] + 10];
  assert 0 <= i < |r| && r[i := r[i] - 10] == s;
  r := r[i := r[i] - 10];
  assert r == s;
}

// By the way, strings are just a special kind of sequence in Dafny: 'seq<char>'.

// We also have sets, just like in Python (though with some syntactic differences).
method Equal?_by_Set(a: int, b: int) returns (result: bool)
  ensures result == (a == b)
{
  return |{a, b}| == 1;
  // Tricky way to compute equality, huh?
}

// Foreshadowing a pattern we'll learn a lot more about in the coming weeks, we
// can essentially use method specifications to check mathematical theorems.
method Facts_about_Set(s: set<int>, t: set<int>, u: set<int>)
  ensures s + t == t + s                   // '+' is union.
  ensures s * t == t * s                   // '*' is intersection.
  ensures s * (t + u) == s * t + s * u     // distributivity
  ensures 7 !in s ==> |s + {7}| == |s| + 1 // membership
  ensures s <= s + t + u                   // subset
{
  // We don't actually need to write any code here.
  // If we did, we could still calculate formulas using set operators!
}

// Most unusually, there are multisets (as we used to express correctness of
// sorting).  Multisets are like sets but allow duplicates.  Another way of
// putting it is that multisets are sequences where we forget element order.
method Two_by_Multiset(a: int, b: int) returns (result: int)
  ensures result == 2
{
  return |multiset{a, b}|;
  // This multiset always has two elements, never one!
  // It just might be that the two elements are equal.
}

method Multiset2(m : multiset<int>) returns (m': multiset<int>)
  requires |m| > 0
  ensures m + m != m  // Negation of a set property that doesn't hold for multisets!
  ensures m * m == m  // But this one does.
  ensures |m'| > |m|
{
  m' := m[42 := m[42] + 8];
  // This notation adjusts the count of element 42, to 8 more than it started out.
  // If 42 was not in the original multiset, 'm[42]' evaluates to 0.
}

// Finally, another key data structure is maps, which are an immutable version
// of e.g. dictionaries in Python.
method Map1(ak: int, bk: int, av: int, bv: int) returns (m: map<int, int>)
  requires ak != bk
  ensures |m| == 2
  ensures ak in m
  ensures m[ak] == av
  ensures bk in m
  ensures m[bk] == bv
  ensures m.Keys == {ak, bk}
  ensures m.Values == {av, bv}
  ensures (ak, av) in m.Items
  ensures (bk, bv) in m.Items
  // We snuck in an example of tuples!
{
  m := map[];
  m := m[ak := av];
  m := m[bk := bv];
}

// We can code up a variety of interesting transformations across container types.
method IsDuplicateAt(s: seq<int>, n: int) returns (b: bool)
  requires 0 <= n < |s|
  ensures b == (s[n] in s[..n] || s[n] in s[n+1..])
{
  // This assertion helps Dafny figure out why the method meets
  // its specification.  Think of it like proposing a useful lemma on the way
  // to a theorem.  Dafny doesn't invent the lemmas on its own, but it is able
  // to check them and then use them to prove later facts.
  assert s == s[..n] + [s[n]] + s[n+1..];
  return multiset(s)[s[n]] > 1;
}