spares.dfy

method Foo(x : int) returns (r : int) ensures r > x { 
    r := x + 1;
}

class SparseSet { 
    ghost var spec : set<nat>
    var n : nat
    var dense : array<nat>
    var sparse : array<nat>
    var universe_size : nat

    constructor(size : nat) 
    requires size > 0
    ensures spec == {}
    ensures valid()
    { 
        dense := new nat[size];
        sparse := new nat[size];
        n := 0;
        universe_size := size;
        spec := {};
    }

    method is_member(x : nat) returns (r : bool)
    requires valid()
    requires x < universe_size 
    ensures valid()
    ensures r == (x in spec)
    { 
        r := sparse[x] < n && dense[sparse[x]] == x; 
    }

    method add_member(x : nat) 
    modifies this, this.dense, this.sparse
    requires n < universe_size - 1
    requires valid() 
    requires x < universe_size
    ensures valid() 
    ensures spec == old(spec) + {x}
    { 
        // If we have space to insert a new element, do so.
        var already_inserted := is_member(x);
        if (!already_inserted) { 
            spec := spec + {x};
            sparse[x] := n;
            dense[n] := x; 
            // None of the members of the dense array change, except for the last one.
            assert(forall i : nat :: 0 <= i < n ==> dense[i] == old(dense[i]));
            n := n + 1;
        } 
    }

    method clear() modifies this 
    requires valid() 
    ensures valid() 
    ensures spec == {}
    {
        spec := {};
        n := 0;
    }


    ghost predicate valid() reads this, this.dense, this.sparse { 
        universe_size == dense.Length && 
        sparse.Length == dense.Length && 
        n < universe_size &&
        arrays_non_aliased() &&
        (forall i : nat :: 0 <= i < n ==> dense[i] < universe_size) &&
        dense_invariant() &&
        (forall i : nat :: i < universe_size ==> (i in spec) == (sparse[i] < n && dense[sparse[i]] == i))
    }

    ghost predicate dense_invariant() reads this, this.dense, this.sparse 
    requires universe_size == dense.Length
    requires n < universe_size
    { 
        (set i : nat | 0 <= i < n :: dense[i]) == spec
    }

    ghost predicate arrays_non_aliased() reads this, this.dense, this.sparse { 
        dense != sparse
    }

}


class ArraySet { 
    ghost var spec: set<nat>
    var arr : array<bool>


    constructor(n : nat) 
    ensures valid()
    ensures spec == {}
    { 
        spec := {};
        var arr := new bool[n];
        var i := 0; 
        while (i < arr.Length) 
        invariant 0 <= i <= arr.Length
        invariant forall j : nat :: j < i ==> arr[j] == false
        {
            arr[i] := false;
            i := i + 1;
        }
        this.arr := arr;
    }

    method insert(x : nat) returns (r : bool)
    requires valid()
    ensures valid()
    ensures r ==> spec == old(spec) + {x}
    ensures !r ==> spec == old(spec)
    modifies this
    modifies this.arr
    { 
        if (x < this.arr.Length) { 
            spec := spec + {x};
            arr[x] := true;
            r := true;
        } else { 
            r := false;
        }
    }
    
    method is_member(x : nat) returns (r : bool) 
    requires valid() 
    ensures valid() 
    ensures r == (x in spec)
    { 
        if (x < this.arr.Length) { 
            r := arr[x];
        } else { 
            r := false;
        }
    }

    method clear() 
    ensures valid()
    ensures spec == {}
    modifies this
    modifies this.arr
    { 
        var i := 0; 
        while (i < arr.Length) 
        invariant 0 <= i <= arr.Length
        invariant forall j : nat :: j < i ==> arr[j] == false
        modifies this.arr
        {
            this.arr[i] := false;
            i := i + 1;
        }
        this.spec := {};
    }

    ghost predicate valid() 
    reads this
    reads this.arr
    { 
        (set x : int | 0 <= x < this.arr.Length && this.arr[x] == true) == spec
    }

}