Formal Definition of Programming Languages

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
--

Return to the comp.compilers page.
Search the comp.compilers archives again.