Go backward to Semantics of Type Declarations Go up to Top Go forward to Declarations

Semantics of Type Declarations

get-storage: Nat -> Array -> Store ->
    (Denotable-value x Poststore)
get-storage = lambda n.lambda a.lambda s. n greater n₂ ->
    (inArray(a), return s)
    [] let (d, p) = T[[T]]s
        in (check(get-storage (n plus one)
            (augment-array n d a)))(p)

augment-array: Nat -> Denotable-value ->
    Array -> Array
augment-array = lambda n.lambda d.lambda (map, lower, upper).
    ([n |->d]map, lower, upper)
empty-array: Nat -> Nat -> Array
empty-array = lambda n₁.lambda n₂.((lambda n.inErrvalue()), n₁, n₂)

• get-storage iterates from lower bound of array to upper bound allocating the proper amount of storage for a component.
• augment-array inserts the component into the array.