// Simple.dfy

class MyClass<T, U> {
  var x: int

  method M(s: bool, lotsaObjects: set<object>)
      returns (t: object, u: set<int>, v: seq<MyClass<bool,U>>)
    requires s
    modifies this, lotsaObjects
    ensures t == t
    ensures old(null) != this
  {
    x := 12;
    while x < 100
      invariant x <= 100
    {
      x := x + 17;
      if x % 20 == 3 {
        x := this.x + 1;
      } else {
        this.x := x + 0;
      }
      t, u, v := M(true, lotsaObjects);
      var to: MyClass<T,U>;
      to, u, v := this.M(true, lotsaObjects);
      to, u, v := to.M(true, lotsaObjects);
      assert v[x] != null ==> null !in v[2 .. x][1..][5 := v[this.x]][..10];
    }
  }

  function F(x: int, y: int, h: WildData, k: WildData): WildData
  {
    if x < 0 then
      h
    else if x == 0 then
      if if h == k then true else false then
        h
      else if y == 0 then
        k
      else
        h
    else
      k
  }
}

datatype List<T> = Nil | Cons(T, List<T>)

datatype WildData = Something | JustAboutAnything(bool, myName: set<int>, int, WildData) | More(List<int>)

class C {
  var w: WildData
  var list: List<bool>
}

class CF {
  static function F(): int

  predicate method G()

  copredicate Co(): bool

  protected function H(): int

  static protected function method I(): real

  static protected predicate method J()
}

lemma M(x: int)
  ensures x < 8
{
}

colemma M'(x': int)
  ensures true
{
}

Dafny program verifier finished with 0 verified, 0 errors