// chalice-parameter=-defaults -autoFold -autoMagic
// verify this program with -defaults -autoFold -autoMagic

class Cell module Library {
  var x: int;

  method init(v: int)
    requires acc(this.x) && 0<=v;
    ensures valid && this.get() == v;
  {
    x := v;
  }

  method set(v: int)
    requires valid && 0<=v;
    ensures valid && get()==v;
  {
    x := v;
  }
  
  method increment()
    requires valid;
    ensures valid && get() == old(get()) + 1;
  {
    x := x + 1;
  }

  method dispose()
    requires valid && acc(mu);
    ensures true;
  {
    free this;
  }

  function get(): int
    requires valid;
    ensures 0<=result;
  {
    x
  }

  predicate valid {
    acc(this.x) && 0<=x
  }

  invariant valid;
}

class Interval module Library2 {
  var left: Cell;
  var right: Cell;

  method init(l: int, r: int)
    requires 0<=l && l <= r;
    requires acc(left) && acc(right);
    ensures valid;
    ensures getLeft()==l
    ensures getRight()==r;
  {
    left := new Cell;
    call left.init(l);
    right := new Cell;
    call right.init(r);
  }

  method setLeft(l: int)
    requires valid;
    requires 0<=l && l<=getRight();
    ensures valid;
    ensures getLeft()==l && getRight()==old(getRight());
  {
    call left.set(l);
  }

  method setRight(r: int)
    requires valid;
    requires 0<=r && getLeft()<=r;
    ensures valid;
    ensures getLeft()==old(getLeft()) && getRight()==r;
  {
    call right.set(r);
  }

  method shift(v: int)
    requires valid;
    requires 0<=v;
    ensures valid;
    ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;
  {
    call left.set(left.get()+v);
    call right.set(right.get()+v);
  }

  function getLeft() : int
    requires valid;
  {
    left.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
  }

  function getRight() : int
    requires valid;
  {
    right.get() // for some reason, Boogie can't figure out the callee's heap is smaller when using defaults
  }
  
  predicate valid
  {
    left.valid && right.valid && left.get() <= right.get()
  }
}

class Program module Main {
  method main(){
    var c1 := new Cell;
    call c1.init(5);
    call c1.set(6);

    var c2 := new Cell;
    call c2.init(10);
    call c2.set(11);

    assert c1.get() == 6;
  }

  method main2(){
    var c: Cell;

    c := new Cell;
    call c.init(0);
    call c.dispose();

    assert c.valid; // should fail
  }

  method main3() returns (rt: Cell)
    ensures rt!=null && rt.valid && rt.get() == 0
  {
    rt := new Cell;
    call rt.init(0)
  }

  method main4() {
    var c: Cell;

    c := new Cell;
    call c.init(0);
    share c;

    acquire c;
    call c.set(1);
    release c;
  }
}