This Article 
 Bibliographic References 
 Add to: 
March 1976 (vol. 2 no. 1)
pp. 33-40
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.
Index Terms:
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
Usage of this product signifies your acceptance of the Terms of Use.