///////////////////////////////////////////////////////////////////////////
// Basic counter
///////////////////////////////////////////////////////////////////////////

class Counter
{
    var incs: int;
    var decs: int;


    ghost var Value : int;

    predicate Valid()
        reads this
    {
        Value == incs - decs
    }

    constructor ()
        ensures Valid()
        ensures Value == 0
    {
        incs, decs, Value := 0, 0, 0;
    }

    method getValue() returns (x: int)
        requires Valid()
        ensures x == Value
    {
        x := incs - decs;
    }

    method inc()
        modifies this
        requires Valid()
        ensures Valid()
        ensures Value == old(Value) + 1
    {
        incs, Value := incs + 1, Value + 1;
    }

    method dec()
        modifies this
        requires Valid()
        ensures Valid()
        ensures Value == old(Value) - 1
    {
        decs, Value := decs + 1, Value - 1;
    }

    method Main()
    {
        var c := new Counter();
        c.inc(); 
        c.inc();
        c.dec();
        c.inc();
        var x := c.getValue();
        assert x == 2;
        assert c.Valid();
    }
}



///////////////////////////////////////////////////////////////////////////
// Counter with cells
///////////////////////////////////////////////////////////////////////////
class Cell
{
    var data: int;

    constructor (n: int) 
        ensures this.data == n
    {
        this.data := n;
    }
}

class CounterCell
{
    var incs: Cell;
    var decs: Cell;


    ghost var Value : int;

    predicate Valid()
        reads this
        reads incs // PROBLEM: WE ARE EXPOSING THE IMPLEMENTATION IN THE SPEC
        reads decs
    {
        incs != decs && Value == incs.data - decs.data
    }

    constructor ()
        ensures Valid()
        ensures Value == 0
        ensures fresh(incs)
        ensures fresh(decs)
    {
        incs := new Cell(0);
        decs := new Cell(0);
        Value := 0;
    }

    method getValue() returns (x: int)
        requires Valid()
        ensures x == Value
    {
        x := incs.data - decs.data;
    }

    method inc()
        requires Valid()
        modifies this
        ensures Valid()
        ensures Value == old(Value) + 1
        modifies incs // Forces change to valid()
        ensures incs == old(incs) // WE HAVE TO SAY THAT NO NEW REFS ARE CREATED
        ensures decs == old(decs)
    {
        incs.data, Value := incs.data + 1, Value + 1;
    }

    method dec()
        requires Valid()
        modifies this
        modifies decs
        ensures Valid()
        ensures Value == old(Value) - 1
        ensures incs == old(incs) // WE HAVE TO SAY THAT NO NEW REFS ARE CREATED
        ensures decs == old(decs)
    {
        decs.data, Value := decs.data + 1, Value - 1;
    }

    method Main()
    {
        var c := new CounterCell();
        c.inc(); 
        c.inc(); // The problem is that the specs of inc cannot allow inc to 
                 // change to a diff. Cell object
        c.dec();
        c.inc();
        var x := c.getValue();
        assert x == 2;
        assert c.Valid();
    }
}


///////////////////////////////////////////////////////////////////////////
// Counter with dynamic frames
///////////////////////////////////////////////////////////////////////////
class CounterDynamicFrames
{
    var incs: Cell;
    var decs: Cell;


    ghost var Value : int;
    ghost var Repr : set<object>;

    predicate Valid()
        reads this, Repr
    {
        this in Repr && 
        incs in Repr && decs in Repr &&
        incs != decs && Value == incs.data - decs.data
    }

    constructor ()
        ensures Valid() && fresh(Repr - {this})
        ensures Value == 0
    {
        incs := new Cell(0);
        decs := new Cell(0);
        Value := 0;

        Repr := {this};
        Repr := Repr + {incs, decs};
    }

    method getValue() returns (x: int)
        requires Valid()
        ensures x == Value
    {
        x := incs.data - decs.data;
    }

    method inc()
        requires Valid() 
        modifies Repr
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Value == old(Value) + 1
    {
        incs.data, Value := incs.data + 1, Value + 1;
    }

    method dec()
        requires Valid()
        modifies Repr
        ensures Valid() && fresh(Repr - old(Repr))
        ensures Value == old(Value) - 1
    {
        decs.data, Value := decs.data + 1, Value - 1;
    }

    method Main()
    {
        var c := new CounterDynamicFrames();
        c.inc(); 
        c.inc();
        c.dec();
        c.inc();
        var x := c.getValue();
        assert x == 2;
        assert c.Valid();
    }
}