A simple ALGOL-like language is defined which includes conditional, while, and procedure call statements as well as blocks. A formal interpretive semantics and a Hoare style axiom system are given for the language. The axiom system is proved to be sound, and in a certain sense complete, relative to the interpretive semantics. The main new results are the completeness theorem, and a careful treatment of the procedure call rules for procedures with global variables in their declarations.
No takes yet. Share an insight, caveat, or question.
Stephen Cook (1978) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: