class Program {
  method main(){
    var buffer := new Queue;
    call buffer.init();
    share buffer;

    var producer := new Producer;
    call producer.init(buffer);
    fork tkP := producer.run();

    var consumer := new Consumer;
    call consumer.init(buffer);
    fork tkC := consumer.run();

    join tkP;
    join tkC;
  
    acquire buffer;
    unshare buffer;

    var tmp := buffer.size();
  }
}

class Producer module Producer {
  var buffer: Queue;

  method init(buff: Queue)
    requires acc(buffer) && buff!=null;
    ensures valid && getBuffer()==buff;
  {
    buffer := buff;
    fold valid;
  }

  method run()
    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
    ensures rd(old(getBuffer()).mu);
  {
    var tmp: int;

    while(true)
      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
    {
      unfold valid;
      acquire buffer;
      call buffer.enqueue(5);
      release buffer;
      fold valid;
    }
    unfold valid;
  }

  function getBuffer(): Queue
    requires valid;
    ensures result!=null;
  {
    unfolding valid in buffer
  }

  predicate valid {
    acc(buffer) && buffer!=null
  }
}

class Consumer module Consumer {
  var buffer: Queue;

  method init(buff: Queue)
    requires acc(buffer) && buff!=null;
    ensures valid && getBuffer()==buff;
  {
    buffer := buff;
    fold valid;
  }

  method run()
    requires valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
    ensures rd(old(getBuffer()).mu);
  {
    while(true)
      invariant valid && rd(getBuffer().mu) && waitlevel << getBuffer().mu;
    {
      unfold valid;
      acquire buffer;
      if(0<=buffer.size()){
        call buffer.enqueue(5);
      }
      release buffer;
      fold valid;
    }
    unfold valid;
  }

  function getBuffer(): Queue
    requires valid;
    ensures result!=null;
  {
    unfolding valid in buffer
  }

  predicate valid {
    acc(buffer) && buffer!=null
  }
}

class Queue module Queue {
  var contents: List;

  invariant valid;

  method init()
    requires acc(contents);
    ensures valid;
    ensures size()==0;
  {
    contents := new List;
    call contents.init();
    fold valid;
  }

  method enqueue(x: int) 
    requires valid;
    ensures valid;
    ensures size() == old(size())+1;
  {
    unfold valid;
    call contents.add(x);
    fold valid;
  }

  method dequeue() returns (rt: int)
    requires valid && 0<size();
    ensures valid;
    ensures size() == old(size())-1;
  {
    unfold valid;
    call rt := contents.removeFirst();
    fold valid;
  }

  function size(): int
    requires valid;
  {
    unfolding valid in contents.size()
  }

  predicate valid {
    acc(contents) && contents!=null && contents.valid
  }
}

class List module Collections {
  var contents: seq<int>;

  method init()
    requires acc(contents);
    ensures valid && size()==0;
  {
    contents := nil<int>;
    fold valid; 
  }

  method add(x: int) 
    requires valid;
    ensures valid && size() == old(size()+1) && get(size()-1) == x;
    ensures forall i in [0..size()-1] :: get(i) == old(get(i));
  {
    unfold valid;
    contents := contents ++ [x];
    fold valid;
  }

  method removeFirst() returns (rt: int) 
    requires valid && 0<size();
    ensures valid && size() == old(size()-1);
    ensures forall i in [0..size()] :: get(i) == old(get(i+1));
  {
    unfold valid;
    rt := contents[0];
    contents := contents[1..];
    fold valid;
  }


  function get(index: int): int 
    requires rd(valid) && 0<=index && index<size();
  {
    unfolding rd(valid) in contents[index]
  }

  function size(): int 
    requires rd(valid);
    ensures 0<=result;
  {
    unfolding rd(valid) in |contents|
  }

  predicate valid {
    acc(contents)
  }
}