Relarray

module array(domain,range) = {

    type this
    alias t = this

return an empty array

    action empty returns (a:t)

return an array with end=s and all values mapped to y

    action create(s:domain,y:range) returns (a:t)

mutate an array a so that x in [0,end) maps to y

    action set(a:t,x:domain,y:range) returns (a:t)

get the value y such that x in [0,end) maps to y in array a

    action get(a:t,x:domain) returns (y:range)

get the value of end

    action size(a:t) returns (s:domain)

change the size of the array

    action resize(a:t,s:domain,v:range) returns (a:t)

add one element to the array

    action append(a:t,v:range) returns (a:t)

Representation

Function "end" gives the end value of an array while value(a,x) gives the value that x maps to in a.

    function end(A:t) : domain
    relation value(A:t,X:domain,Y:range)

Specification

Notice that get and set have the precondition that x is in [0,end).

    object spec = {
    property end(X) >= 0
        property value(A,X,Y1) & value(A,X,Y2) -> Y1 = Y2

    after empty {
        assert end(a) = 0
    }
    before create {
        assert 0 <= s
    }
    after create {
        assert end(a) = s & value(a,X,y)
    }
        before set {
        assert 0 <= x & x < end(a)
    }
    after set {
            assert end(a) = end(old a);
        assert value(a,x,Y) <-> Y = y;
            assert X ~= x -> (value(a,X,Y) <-> value(old a,X,Y))
    }
    before get {
        assert 0 <= x & x < end(a)
    }
    after get {
        assert value(a,x,y)
    }
    after size {
        assert s = end(a)
    }
    after resize {
        assert end(a) = s;
        assert 0 <= X & X < end(old a) -> value(a,X,Y) <-> value(old a,X,Y);
        assert end(old a) <= X & X < s -> value(a,X,Y) <-> Y = v
    }
    after append {
        assert end(a) > end(old a) & ~(end(old a) < X & X < end(a));
        assert 0 <= X & X < end(old a) -> value(a,X,Y) <-> value(old a,X,Y);
        assert value(a,end(old a),Y) <-> Y = v
    }
    }

    object impl = {

object t_ = {}

<<< member class t_ : std::vector<range> {};

interpret t -> <<< t_ >>>

    interpret t -> <<< std::vector<`range`> >>>

    definition value(a:t,i:domain,v:range) = <<< (0 <= `i` && `i` < `a`.size()) ? `a`[`i`] == `v`: false >>>

    definition end(a:t) = <<< `a`.size() >>>

    implement create {
        <<<
            `a`.resize(`s`);
            for (unsigned i = 0; i < `s`; i++)
                `a`[i] = y;
        >>>
    }

    implement empty {
        <<<
        >>>
    }

    implement set {
        <<<
            if (0 <= `x` && `x` < (`domain`)`a`.size())
                `a`[`x`] = `y`;
        >>>
    }

    implement get {
        <<<
            if (0 <= `x` && `x` < (`domain`)`a`.size())
                `y` = `a`[`x`];
        >>>
    }

    implement size {
        <<<
            `s` = (`domain`) `a`.size();
        >>>
    }

    implement resize {
        <<<
            unsigned __old_size = `a`.size();
            `a`.resize(`s`);
            for (unsigned i = __old_size; i < (unsigned)`s`; i++)
                `a`[i] = v;
            >>>
        }

    implement append {
        <<<
            `a`.push_back(`v`);
            >>>
        }

    <<< impl
        std::ostream &operator <<(std::ostream &s, const `t` &a) {
            s << '[';
        for (unsigned i = 0; i < a.size(); i++) {
            if (i != 0)
                s << ',';
            s << a[i];
        }
            s << ']';
        return s;
            }

        template <>
        `t` _arg<`t`>(std::vector<ivy_value> &args, unsigned idx, int bound) {
            ivy_value &arg = args[idx];
            if (arg.atom.size())
                throw out_of_bounds(idx);
            `t` a;
            a.resize(arg.fields.size());
        for (unsigned i = 0; i < a.size(); i++) {
            a[i] = _arg<`range`>(arg.fields,i,0);
            }
            return a;
        }

        template <>
        void __deser<`t`>(ivy_deser &inp, `t` &res) {
            inp.open_list();
            while(inp.open_list_elem()) {
            res.resize(res.size()+1);
                __deser(inp,res.back());
            inp.close_list_elem();
                }
        inp.close_list();
        }

        template <>
        void __ser<`t`>(ivy_ser &res, const `t` &inp) {
            int sz = inp.size();
            res.open_list(sz);
            for (unsigned i = 0; i < (unsigned)sz; i++) {
            res.open_list_elem();
                __ser(res,inp[i]);
            res.close_list_elem();
                }
            res.close_list();
        }

ifdef Z3PP_H_

        template <>
            z3::expr __to_solver(gen& g, const z3::expr& z3val, `t`& val) {
            z3::expr z3end = g.apply("`end`",z3val);
            z3::expr __ret = z3end  == g.int_to_z3(z3end.get_sort(),val.size());
            unsigned __sz = val.size();
            for (unsigned __i = 0; __i < __sz; ++__i)
            __ret = __ret && __to_solver(g,g.apply("`value`",z3val,g.int_to_z3(g.sort("`domain`"),__i)),val[__i]);
                return __ret;
            }

        template <>
        void  __from_solver<`t`>( gen &g, const  z3::expr &v,`t` &res){
            `domain` __end;
            __from_solver(g,g.apply("`end`",v),__end);
            unsigned __sz = (unsigned) __end;
            res.resize(__sz);
            for (unsigned __i = 0; __i < __sz; ++__i)
            __from_solver(g,g.apply("`value`",v,g.int_to_z3(g.sort("`domain`"),__i)),res[__i]);
        }

        template <>
        void  __randomize<`t`>( gen &g, const  z3::expr &v){
            unsigned __sz = rand() % 4;
                z3::expr val_expr = g.int_to_z3(g.sort("`domain`"),__sz);
                z3::expr pred =  g.apply("`end`",v) == val_expr;
                g.add_alit(pred);
            for (unsigned __i = 0; __i < __sz; ++__i)
                __randomize<`range`>(g,g.apply("`value`",v,g.int_to_z3(g.sort("`domain`"),__i)));
        }

endif

    >>>
    }

    trusted isolate iso = spec,impl

    attribute test = impl
}