Issue No.01 - March (1976 vol.2)
J.M. Spitzen , Computer Science Group, Stanford Research Institute
The problem of applying formal techniques of program specification and verification to large complex programs is considered. It is argued that a practical solution requires a variety of techniques, including both procedural and nonprocedural specifications, hierarchical program organization, and the use of program transformations. In particular, a case is made for flexible problem-oriented choice of specification techniques and languages. These ideas are expanded by specifying a load-and-go assembler in three parts: a transduction grammar describing the correspondence between concrete and abstract syntax for assembly language programs; a set of transformations of the abstract form; and a nonconstructive axiomatic specification of the result of core assembly and loading of transformed abstract programs.
abstract syntax, Assemblers, program verification, formal specification, transduction grammars, program transformation
J.M. Spitzen, "The Specification of Assemblers", IEEE Transactions on Software Engineering, vol.2, no. 1, pp. 33-40, March 1976, doi:10.1109/TSE.1976.233799