Seg3

include order
include collections


module segment2(domain,range,arr) = {

Requirements

• Type domain must support arithmetic.
• Type arr must be an array type over (domain,range).

This is a type of segments over arr

    type this

Extract a segment of an array, from a begin index to an end index

    action make(data:arr, begin:domain, end:domain) returns (seg:this)

Function to obtain the value of a segment at a given index.

    function value(X:this,N:domain) : range

    function first(X:this) : domain
    function upper(X:this) : domain

    specification {

When extracting a segment from an array, the range [begin,end) must describe a segment of the array. The return value is a segment representing the range [begin,end) of the array

Example:

var a := arr.empty
a := a.append(1);
a := a.append(2);
a := a.append(3);
a := a.append(4);
var s := segment.make(a,1,3);
assert s.value(1) = 2 & s.value(2) = 3;   -- true
assert s.value(0) = 1;                    -- false
assert s.value(3) = 4;                    -- false

        around make {
            require 0 <= begin & begin <= end & end <= data.end
            ...
            ensure begin <= N & N < end -> value(seg,N) = arr.value(data,N);
            ensure first(seg) = begin;

TODO: uncomment the next line and get an OOM error

            ensure upper(seg) = end;
        }
    }

    implementation {

The implementation represents a segment as a pair consisting of an offset into the original array and an array containin the segment values. It constructs segmens in the expected way, by copying array elements in a loop.

We have to use arithmetic to prove the implementation, but this is within the decidable array property fragment.

Notice we use domain.impl to prove this isolate, so we get the arithmetic theory.

        destructor offset(X:this) : domain
        destructor elems(X:this) : arr

        definition value(X,n:domain) = elems(X).value(n - offset(X))

        definition first(X) = offset(X)

        definition upper(x:this) = (elems(x).end) + offset(x)

        implement make {
            seg.offset := begin;
            seg.elems := arr.empty;
            var idx := begin;
            while idx < end
            invariant begin <= idx & idx <= end
            invariant seg.offset = begin
            invariant begin <= N & N < idx -> seg.value(N) = data.value(N)
            invariant begin + seg.elems.end = idx
            {
                seg.elems := seg.elems.append(data.value(idx));
                idx := idx.next;
            };
        }
    }

    isolate iso = this with domain.impl,arr
}


instance dom : unbounded_sequence
type rng
instance arr : array(dom,rng)

instance s : segment2(dom,rng,arr)

export s.make