Proof obligations for blocks and procedures
Alain Ah-kee · Formal Aspects of Computing · 1990
Abstract Operation decomposition proof obligations are given for a language with blocks and unrestricted procedure calls with reference parameters and global variables. Post-conditions of the initial and final states of the computation are used; existing proof rules are for post-conditions which are predicates of the final state only. Aliasing, as arising from reference parameters, and static scoping are dealt with in the Hoare-like proof system by the use of a “syntactic environment”.