translation rules
statements
S ? a ; b ? = S ? a ? ; S ? b ?
S ? if p a b ? = (P ? p ? ? S ? a ?) ? (! P ? p ? ? S ? b ?)
S i ? while p { a } ? = (P ? p ? ? S ? a ? ; S i-1 ? while p { a } ?) ? Close (! P ? p ?)
S 0 ? while p { a } ? = Close (! P ? p ?)
S ? v = t ? = Close (v’ = E ? t ?)
S ? t.f = u ? = Close (E ? t ? . f’ = E ? u ? ? all x | x != E ? t ? -> x.f = x. f’)
expressions
E ? v ? = v
E ? t.f ? = E ? t ? . f
predicates
P ? t == u ? = (E ? t ? = E ? u ?)
P ? !p ? = ! P ? p ?
Close (F) = F && v’ = v && all x | x.f = x.f’ (all v, f not appearing primed in F)