The Specification of Assemblers
Jay M. Spitzen · IEEE Transactions on Software Engineering · 1976
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.