when a abstract construct has no user postcondition
we try to add one by purifying the program expression,
that is, ensures { result = t }, where t is a term
obtained from the program expression e

program expression e may involve function calls with
preconditions (e.g. array access, division)

the purpose of this change is to limit the number
of VCs by surrounding some program expressions with
abstract (e.g. if abstract i >= 0 && a[i] = 0 end then ...)

this is not a conservative change: one may have to
add ensures { true } to recover the previous behavior
(yet there is no example in the gallery of abstract e
with e pure and no post)

note: we might want to do that automatically for if-then-else
expressions (including lazy operators)