holt@turing.toronto.edu (Ric Holt) (01/25/89)
Greg Cowin writes: >Overlooking the real problem of defining a programming language >seems to be very common. The problem is providing a formal >semantic definition. This problem is not easily solved, although >it can be done. I think the Turing experience in language design is relevant here. This language was designed, from the beginning, to have a formal definition. LANGUAGE DESIGN FOR FORMALISM: This means that many features that are almost impossible to formalize in other languages were "tamed" in the early design of Turing; an example of this is Turing's treatment of pointers as a special kind of subscript rather than as machine addresses. STRUCTURE OF FORMAL DEFINITION: The formal definition of Turing has this structure: FORMAL SYNTAX: This consists of LEXICAL DEFINITION: What are tokens, comments and separators CONTEXT FREE DEFINITION: The BNF CONTEXT CONDITIONS: Type checking etc. Sometimes called static semantics or context sensitive syntax. FORMAL SEMANTICS: This consists of VALIDITY PREDICATES: What's illegal at runtime, eg, subscripts must be in bounds, division by zero is illegal, etc. BASIS STATEMENTS: Ten fundamental statements (eg, unchecked assignment and unchecked IF) used as the basis of defining all other statements. These ten statements are defined both operationally (so you know how to write a correct compiler) and using weakest pre conditions (so you know how to write a correct program). AXIOMS: These define operators such as + and the corresponding types, including integers, real numbers, enumerated types, arrays, records, etc. STATEMENT DEFINITIONS: All Turing statements and declarations are defined in terms of the above (or in terms of previously defined statements). All of this is explained in excruciating detail in the book "The Turing Programming Language: Design and Definition" [Prentice-Hall], which I hope you'll buy lots of copies of so I'll get rich :-) The high speed Turing compiler was developed by opening this book and "transliterating" these definitions into an implementation (while applying a few dozen years of compiler know-how to make it all work). Ric Holt, Dept of Comp Sci, Univ of Toronto, Room 2001, Sandford-Fleming Bldg, Toronto, Canada M5S 1A4 holt@turing.toronto.edu -- Send compilers articles to ima!compilers or, in a pinch, to Levine@YALE.EDU Plausible paths are { decvax | harvard | yale | bbn}!ima Please send responses to the originator of the message -- I cannot forward mail accidentally sent back to compilers. Meta-mail to ima!compilers-request