Wed, 25 Jan 89 09:40:44 EST

Related articles |
---|

Formal Definition of Programming Languages holt@turing.toronto.edu (Ric Holt) (1989-01-25) |

From: | Ric Holt <holt@turing.toronto.edu> |

Organization: | University of Toronto, CSRI |

Date: | Wed, 25 Jan 89 09:40:44 EST |

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

--

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.