Description The specification states that immediately before the execution of statement (i.e. in the statement’s “prestate”) formula holds.
Pragmatics The specification creates an additional proof obligation but then also more information for the verification of statement and its successors.