class Cell
{
    var inner: InnerCell;
    
    predicate inv
    {
        acc(inner) && inner!=null && rd(inner.value,1) && rd*(inner.mu) && rd*(this.mu)
    }
    
    method CellConstructor()
        requires acc(inner) && acc(this.mu)
        ensures inv && get()==0;
    {
        inner := new InnerCell;
        call inner.InnerCellConstructor(0)
        share inner;
        fold inv;
    }
    
    method CellConstructor2(other: Cell)
        requires acc(inner) && acc(this.mu)
        requires other != null && other.inv;
        requires unfolding other.inv in waitlevel << other.inner.mu
        ensures inv && other.inv && get()==other.get();
    {
        unfold other.inv;
        inner := other.inner;
        acquire inner;
        inner.refCount := inner.refCount+1;
        release inner;
        fold other.inv;
        fold inv;
    }
    
    function get():int
        requires inv;
    { unfolding inv in inner.value }
    
    method set(x:int)
        requires inv;
        requires unfolding inv in waitlevel << inner.mu
        ensures inv && get()==x;
    {
        var old_in: InnerCell;
        unfold inv;
        old_in := inner;
        acquire old_in;
        if (inner.refCount==1) { inner.value:=x; }
        else
        {
            inner.refCount := inner.refCount-1;
            inner := new InnerCell;
            call inner.InnerCellConstructor(x)
            share inner;
        }
        release old_in;
        fold inv;
    }
}

class InnerCell
{
    var value: int;
    var refCount: int;
    
    invariant acc(refCount) && refCount > 0 && acc(value,100-rd(refCount));
    
    method InnerCellConstructor(val: int)
        requires acc(refCount) && acc(value)
        ensures acc(refCount) && acc(value) && refCount==1 && value == val;
    {
        refCount := 1;
        value := val
    }
}