Understanding ALGOL: A View of a Recent Convert to Denotational Semantics

Abstract

The advantages of denotational over copy-rule semantics are argued. A denotational semantics is indicated for an ALGOL-like language with finite-mode procedures, blocks with local storage, and sharing (aliasing). Procedure declarations are completely explained in the usual framework of complete partial orders, but cpo's are inadequate for the semantics of blocks, and a new class of store models is described. The semantics justifies a proof system for partial correctness of commands containing global procedures.