Correctness of Translations of Programming Languages -- An Algebraic Approach
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Programming languages and their sets of meanings can be modelled by general operator algebras seismic functions and compiling functions by homomorphisms of operator algebras. A restricted class of individual programs, machines, and computations can be modelled in a uniform manner by binary relational algebras. These two applications of algebra to computing are compatible the semantic function provided by interpreting running one binary rational algebra on another is a homomorphism on an operator algebra whose elements are binary relational algebras. Under these mathematical tools, proofs can be provided systematically of the correctness of compilers for fragmentary programming languages, each embodying a single language feature. Exemplary proofs are given for statement sequences, arithmetic expressions, Boolean expressions, assignment statements, and statements. Moreover, proofs of this sort can be combined to provide synthetic proofs for, in principle, many different complete programming languages. One example of such a synthesis is given.
- Computer Programming and Software