Preliminaries

1. Name
2. Location
3. What theory courses
4. What mathematics courses
5. What computer language courses

Text
Introduction to the Theory of Programming Languages, Bertrand Meyer, Prentice Hall, 1990, ISBN 0-13-498510-9

Course Description

Seminar in the definition and philosophy of grammars, contextual relationships, semantic and syntactic analysis, parsing efficiency analysis, and program verification.
If time allows, intractability and the classes of P, NP-Hard, NP-Complete.

Syllabus

1. Abstract Syntax: Backus-Naur Form (BNF) Grammars
2. Attribute Grammars
3. Syntax to Semantics: Translational Semantics
4. Operational Semantics
5. Denotational Semantics
6. Axiomatic Semantics
7. Program Analysis and Verification
8. Computational Complexity and Intractability

"Given that programming languages are strictly artificial entities created to facilitate the preparation of computer programs and the representation and communication of algortihms, their diversity, complexity, and often unfathomed depth of structure and concept are truly remarkable. After three decades of intense research and development, there is still no end in sight to the stream of useful innovations in language design and valuable theoretical insights into language structure." [Pagan] Pagan, Frank, Formal Specification of Programming Languages, Prentice-Hall, Inc., 1981.

Chapter 1: Basic Concepts

When writing a definitive specification or standard definition of a language, the informal approaches have well-known disadvantages.

• lack of clarity and precision
• natural language is too vague and imprecise to express the intricate and detailed properties of programing languages completely, exactly, and unambiguously

One requires formal methods if there is to be any hope of being able to write language specifications with the following qualities:

• completeness
• consistency
• precision
• absence of ambiguity
• conciseness
• understandability
• usefulness

Informal specs are verbose and often vague... and none of the above :-)

"The formal descriptions discussed in this book are mathematical theories used to model and analyze the essential properties of programming languages and programs." text

Two points formal and essential:

Why do we want such precise (formal) definitions of programming languages?

1. Help in understanding languages
   raise questions that might not be asked in informal

2. Support for language standardization
   key to portability is standardization
   "Standardization, if effectively conceived and implemented, can inhibit the unruly proliferation of ill-defined and incompatible dialects provided by different implementations and described in different expositions, thus increasing the language's value as a medium of communication and a tool for writing portable programs. It is now generally accepted that standardization efforts can be really successful only if they are provided with an adequate technical basis, and this means that they must employ formal specification techniques to one extent or another." [pagan]

3. Guidelines for language design
   mathematical simplicity in specs provide 'clean' languages
   "It can expose language irregularities not apparent from the surface, reveal underlying similarities between apparently different languages and differences between apparently similar languages, and isolate the reasons why certain combinations of facilities give rise to complex or inconsistent interactions, why the use of a certain feature in programs is difficult to prove correct, and so forth." [pagan]

4. Aid in writing compilers and language systems
   formal descriptions viewed as specs of an abstract language system for that language - can lead to Automatic synthesis

5. Support for program verification and software reliability
   proofs of programs and correctness of implementations

6. Model for software specification
   Language reference
   • for users
   • for implementers

In the definition of a language, one requires precision and absense of ambiguity (at which mathematical techniques are particularly effective) without commitment to a particular implementation, i.e., without overspecification.

The emphasis on essential features restricts the discussion to properties that characterize programs and programming languages independently of particular implementations.

Basic categorization of the various aspects of language description:

• syntax - deals with questions of superficial form
  (the structure of well-formed programs)

• semantics - deals with questions of meaning
  (meaning of meaning?)

• pragmatics - deals with the practical use

Example: Consider the following instance of the common assignment statement:

a := b + sin (x) + 2
• Syntax.. An assignment statement consists of a variable followed by the symbol ':=' followed by an expression.

• Semantics. The execution of an assignment statement consists of evaluating the expression on its right side and causing the resulting value to be associated with the variable on its left side, thus superseding any value previously associated with the variable.

• Pragmatics. An assignment statement may be used to compute and retain the value of an invariant expression that is needed at more than one point in a program, or to update the value in terms of its previous value, or ...

Of course, descriptions of "variable" and "expression" would also need to be supplied...

Any kind of description or specification of a language must employ some metalanguage.

A metalanguage is any language or notation used to describe programming languages.

A formal description requires a formal metalanguage.

What we will study in this course are informal explanations of formal metalanguages and examples of their use in defining programming languages. (more later)

Mathematics vs. Programs

Imperative features: (page 6)

characterized by the presence of constructs describing commands:
• instructions
  note: instruction vs. statement (facts)
• explicit sequencing
• assignment (vs. equality)
  note: side effects in programming

Referential transparency

substitutivity of equals for equals: note examples on page 7 & 8
aliasing (e.g., passing by reference)

A word of warning:
Throughout this course one will need to be careful about when one is using metalanguage and when one is using the language being defined.

Formal specifications tend to use many of the notions used for programming purposes.

Example: page 11 Case "statements"

We will define the metalanguage terminology, which uses abstract syntax, in Chapter 3 when we define the metalanguage Metanot.