Creport3

include order
include collections

module shift_theory(idx) = {
    relation r(T : idx, X : idx, Y : idx)
    action f(t:idx,x:idx) returns (y:idx)

    specification {
    property r(T,X,Y) & r(T,X,Y1) -> Y = Y1
    property r(T,X,Y) & r(T,X1,Y) -> X = X1
    property r(T,X1,Y1) & r(T,X2,Y2) & X1 < X2 -> Y1 < Y2
    property r(T1,X,Y1) & r(T2,X,Y2) & T1 < T2 -> Y2 < Y1
        property r(T,X1,Y1) & idx.succ(X1,X2) & idx.succ(Y1,Y2) -> r(T,X2,Y2)
        property r(0,X,X)
        property r(X,X,0)
        property r(T,X,Y) -> Y <= X & T <= X
    around f {
           require t <= x;
            ...
       ensure r(t,x,y)
    }

    } # end specification section
    implementation {
        definition r(T,X,Y) = (X = Y + T)
        implement f {
            y := x - t
        }
    }
    isolate iso = this with idx.impl
}

module mysegment(domain,range,none) = {

    type this

    relation value(S:this,D:domain,R:range)
    relation begin(S:this,D:domain)
    relation end(S:this,D:domain)

    action set(w:this, i:domain, v:range) returns (w:this)
    action read(w:this, i:domain) returns (v:range)
    action trim(w:this, i:domain) returns (w:this)
    action empty(i:domain) returns (w:this)
    action merge(w: this, max_w: this) returns (max_w: this)
    action getBegin(w:this) returns (i:domain)
    action getEnd(w:this) returns (i:domain)

    specification {

        after init {

        }
        around set {
            require v ~= none;
            require exists I. begin(w, I) & I <= i;
        ...
            ensure value(w, I, V) <-> (I = i & V = v) | (I ~= i & value(old w, I, V))
        }
    around read {
            require exists I. begin(w, I) & I <= i;
            ...
            ensure value(w, i, v);
        }
        around trim {
            require exists I. begin(w, I) & I <= i;
            ...
            ensure begin(w, I) <-> I = i;
            ensure value(w, I, V) <-> (i <= I & value(old w, I, V)) | (I < i & V = none);
        }

after empty { ensure value(w, I, V, O) <-> V = none; ensure begin(w, I) <-> I = i; }

around getBegin { ... ensure begin(w, i); }

around getEnd { ... ensure forall I. i <= I -> value(w, I, none); }

        property value(W, I, V1) & value(W, I, V2) -> V1 = V2
        property value(W, I, V) -> 0 <= I
    property begin(W, I) & begin(W, I2) -> I = I2

property end(W, IE) & I >= IE -> value(W, I, none)

    }

    implementation {

        instance shift : shift_theory(slot)
        instance arr : array(domain,range)
        destructor elems(W:this) : arr
        destructor offset(W:this) : domain

        isolate value_abstraction = {
            property X < offset(W) -> value(W,X,none)
            property shift.r(offset(W),X,Y) & Y < elems(W).end -> value(W,X,elems(W).value(Y))
            property shift.r(offset(W),X,Y) & Y >= elems(W).end -> value(W,X,none)
            property value(W, I, V1) & value(W, I, V2) -> V1 = V2
            property value(W, I, V) -> 0 <= I
            theorem [into] {
                property 0 <= I -> exists V. rev(W,I,V)
            }


            implementation {
                definition value(W,X,V) =
                  (exists Y. shift.r(offset(W),X,Y) &
                      (V = elems(W).value(Y) if Y < elems(W).end else none))
                  | X < offset(W) & V = none
            }
        } with shift, arr, domain

        definition begin(W,I) = (I = offset(W))
        definition end(W,I) = shift.r(offset(W),I,elems(W).end)

        implement set {
        var index := shift.f(offset(w), i);
        if w.elems.end <= i {
        w.elems := w.elems.resize(index.next, none);
        };
            w.elems := w.elems.set(index, v);
        }

implement set { var new_end := (i.next) if (i >= elems(w).end) else (elems(w).end); w.elems := w.elems.resize(new_end,none); w.elems := w.elems.set(i-w.offset,v) }

        implement read {
            var index := shift.f(offset(w),i);
        v := none if (index >= w.elems.end) else w.elems.value(index)
        }

implement trim { var j := i; if j <= bound(w) { while j < bound(w) invariant i <= j invariant j <= bound(w) invariant shift.r(offset(w),bound(w),content(w).end) invariant j <= X & X < bound(w) & shift.r(offset(w),X,Y) -> value(old w, X, maxview(content(w).value(Y)), maxop(content(w).value(Y))) invariant i <= X & X < j & shift.r(i,X,Y) -> value(old w, X, maxview(content(w).value(Y)), maxop(content(w).value(Y)) ) invariant bound(w) = bound(old w) invariant offset(w) = offset(old w) invariant content(w).end = content(old w).end { content(w) := content(w).set(shift.f(i,j),content(w).value(shift.f(offset(w),j))); j := j.next; }; content(w) := content(w).resize(shift.f(i,bound(w)),0); offset(w) := i } else { content(w) := arr.empty; offset(w) := i; bound(w) := i; } }

    }

    isolate iso = this with domain
}

instance slot : unbounded_sequence
type data
individual none : data

instance foo : mysegment(slot,data,none)

export foo.set
export foo.read