ListSet.dfy

type Elem = int

/*** Specification ***/

trait SpecSet {
  ghost var content: set<Elem>

  method insert(x: Elem)
    modifies this
    ensures content == old(content) + {x}

  method erase(x: Elem)
    modifies this
    ensures content == old(content) - {x}

  method hasElement(x: Elem)
    returns (result: bool)
    ensures result == (x in content)
}


/*** Implementation based on Lists (possibly with duplicates) ***/

datatype list<T>
  = nil | cons(head: T, tail: list<T>)

function contains(xs: list<Elem>, x: Elem): bool {
  match xs {
    case nil =>
      false
    case cons(y, ys) =>
      x == y || contains(ys, x)
  }
}

function remove(xs: list<Elem>, x: Elem): list<Elem> {
  match xs {
    case nil =>
      nil
    case cons(y, ys) =>
      if x == y then
        remove(ys, x)
      else
        cons(y, remove(ys, x))
  }
}

class ListSet {
  var xs: list<Elem>
  ghost var content: set<Elem>

  ghost predicate Valid()
    reads this
  {
    // predicate representing the inductive invariant
    // (i.e., a forward simulation relation)
    forall x: Elem ::
      contains(xs, x) <==> x in content
  }

  constructor init()
    ensures content == {}
    ensures Valid()
  {
    xs := nil;
    content := {};
  }

  method hasElement(x: Elem)
    returns (result: bool)
    requires Valid()
    ensures result <==> (x in content)
  {
    assert  contains(xs, x) <==> (x in content);

    result := contains(xs, x);

    // our goal: copied from the postcondition,
    // this is what required us to establish an inductive class invariant
    // in the first place (cf. precondition Valid())
    assert result <==> (x in content);
    return result;
  }

  method insert(x: Elem)
    modifies this
    requires Valid()
    ensures Valid()
    ensures content == old(content) + {x}
  {

    xs := cons(x, xs);
    content := content + {x};
  }

  lemma contains_remove_with_explicit_proof(xs: list<Elem>, x: Elem)
    // make inductive measure explicit
    decreases xs

    ensures forall z ::
      contains(remove(xs, x), z) <==> contains(xs, z) && x != z
  {
    // explicit proof
    match xs {
      case nil =>
        // nothing to do
      case cons(y,ys) =>
        // appeal to the inductive hypothesis,
        // which is encoded as a recursive call to ys
        contains_remove_with_explicit_proof(ys, x);

        // now we have
        assert forall z ::
          contains(remove(ys, x), z) <==> contains(ys, z) && x != z;
    }
  }

  lemma contains_remove(xs: list<Elem>, x: Elem)
    ensures forall y ::
      contains(remove(xs, x), y) <==> contains(xs, y) && x != y
  {
    // proved automatically by Dafny using induction on xs
  }

  method erase(x: Elem)
    modifies this
    requires Valid()
    ensures  Valid()
    ensures content == old(content) - {x}
  {
    // the assertions below are *not* necessary to conclude the proof,
    // they just make explicit the respective conditions that are established there

    // invocation of the lemma above for the correct parameters xs, x
    contains_remove(xs, x);

    // unfolding of the predicate valid
    assert forall y :: (y in content && y != x) <==> contains(remove(xs, x), y);

    xs := remove(xs, x);

    // backwards substitution of the assignment below (cf. Hoare Logic)
    assert content - {x} == old(content) - {x};

    content := content - {x};

    // our goal: copied from the postcondition
    assert content == old(content) - {x};
  }
}

SpecSet.dfy

type Elem(==)

class SpecSet {
  ghost var content: set<Elem>

  constructor init()
    ensures content == {}

  method insert(x: Elem)
    modifies this
    ensures content == old(content) + {x}

  method erase(x: Elem)
    modifies this
    ensures content == old(content) - {x}

  method hasElement(x: Elem)
    returns (result: bool)
    ensures result == (x in content)
}