Go backward to Function Domains Go up to Top Go forward to Recursive Function Definitions

Lifted Domains

Unsafe arrays of unsafe values

Domain Uarr = Array_{_|_}

where Array = Nat -> Tr'
and Tr' = (B union {error})_{_|_}

Operations

new-unsafe: Uarr
    new-unsafe = newarray
access-unsafe: Nat_{_|_} -> Uarr -> Tr'
    access-unsafe = lambda n.lambda r.(access n r)
upd-unsf: Nat_{_|_} -> Tr' -> Uarr -> Uarr
    upd-unsf = lambda n.lambda t.lambda r.(update n t r)

Indices and elements may be improper!

upd-unsf(plus one two)(not'(_|_))(new-unsafe)
= upd-unsf(plus one two)(not'(_|_))(newarray)
= upd-unsf(plus one two)(not'(_|_))(lambda n.error)
= upd-unsf(three)(_|_)(lambda n.error)
= update(three)(_|_)(lambda n.error)
= [three |-> _|_](lambda n.error) (not'=lambda t.not(t))