Lifted Domains: Unsafe arrays of unsafe values

Domain Unsafe = Array ? where Array = Nat ? Tr’ and Tr ‘ = (B U {error}) ?

Operations

new­unsafe: Unsafe

new­unsafe = newarray
access­unsafe: Nat ? ? Unsafe ? Tr ’
access­unsafe = ? n. ? r.(access n r)
update­unsafe Nat ? ? Tr ‘? Unsafe ? Unsafe
update­unsafe = ? n. ? t. ? r.(update n t r)

• Note: Indices and elements may be improper! Change this!

Previous slide

Next slide

Back to first slide

View graphic version