Arrayset3

include collections

module set(index,elem) = {

    instance arr:array(index.t,elem)

    alias t = arr.t

    function contains(X:t,y:elem) = exists Z. 0 <= Z & Z < arr.end(X) & arr.value(X,Z) = y

    action emptyset returns(s:t)
    action add(s:t,e:elem) returns (s:t)
    action remove(s:t,e:elem) returns (res:t)

    object spec = {
    after emptyset {
        assert ~contains(s,X)
    }
    after add {
        assert contains(s,X) <-> (contains(old s,X) | X = e)
    }
    after remove {
        assert contains(res,X) <-> (contains(s,X) & X ~= e)
    }
    }

    object impl = {
    implement emptyset {
        s := arr.create(0,0)
    }

    implement add {
        if ~contains(s,e) {
                s := arr.resize(s,index.next(arr.end(s)),e)
        }
        }

    function remove_step (s:t,e:elem,i:index.t,y:elem)
        = (exists Z. 0 <= Z & Z < i & arr.value(s,Z) = y) & y ~= e

    property I >= 0 & index.succ(I,J) ->
        (remove_step(X,E,J,Y) <-> (remove_step(X,E,I,Y) | arr.value(X,I) = Y & Y ~= E))

    property I = arr.end(X) ->
        (remove_step(X,E,I,Y) <-> (contains(X,Y) & Y~=E))

    implement remove {
        local i:index.t, end:index.t {
        i := 0;
        res := arr.create(0,0);
        end := arr.end(s);
        while i < end
            invariant 0 <= i & i <= end
            invariant contains(res,Y) = remove_step(s,e,i,Y)
        {
            local f:elem {
            f := arr.get(s,i);
            if  f ~= e {
                res := add(res,f)
            }
            };
            i := index.next(i)
        }
        }
    }
    }
}

include order

instance index : unbounded_sequence
type elem

instance s : set(index,elem)

export s.emptyset
export s.add
export s.remove

isolate iso_s = s with index
extract iso_impl = s,index