- In this course, we are primarily interested in studying the
meanings of programming languages (e.g., C, C++, C#, Java, Eiffel,
JavaScript, ML, Haskell) and specification languages (e.g., Z,
TLA+, VDM, B, Alloy, CASL, UML).
Note some programming languauges
support static type annotations or "design by contract", that is,
a programmer can annotate various program constructs with some sort
of type information or program assertions. A typechecker or
contract-checker (done at compile- or run time) can be used to help
rule out certain classes of bugs.
Specification languages can be used
to formally build "models" or "blueprints" for any system (not
necessarily software) --- they often come with tools that can be
used to generate test cases, detect bugs, or verify the integrity of
the underlying system.
- Before we can describe the formal semantics of any programming-
or specification language, we first need to pick a
"meta language" --- a language which we can use to define the "meaning"
of the "object" language we are interested in formalizing.
The most common "meta language" for describing mathematical systems
is some sort of set theory formalized using first-order logic, e.g.,
the Zermelo-Fraenkel set theory with axiom of choice.
For this class, we will stick to the familiar set theory as
documented in the Appendix of Reynolds book; we will also assume
the availability of inductive definitioins as discussed in Chapters
1-3 of Harper.
- If you are unhappy with the *informal nature* of the meta language
and meta reasoning we use, you can use a formalized "meta language",
such as the Calculus of Inductive Constructions (CIC) implemented
in the Coq proof assistant. CIC is a rich high-order predicate logic
extended with inductive definitions. Coq allows you to write down
machine-checkable mathematical proofs so that you are sure that
the mathematical reasoning you did is indeed correct (assuming that
the underlying meta logic is consistent and the implementation of
the proof checker is correct).
- The Appendix of Reynolds gets you acquainted with some of the most
important notations and properties in set theory. Reynolds Chapter 1
defines the formal semantics of one sample object language (i.e.,
a first-order predicate logic with integer expressions). This example
language is not a programming language but rather a specification
language (for example, in this language, you don't write programs
but write specifications instead).
- Denotational semantics is to give the meaning of a language by
mapping each "abstract syntax tree" in the object language
into a mathematical object (often called "a denotation") in the
meta language.
For example, In Reynolds Charper 1, there are two semantic functions:
[[ - ]]intexp maps each "intexp" expression into a mathematical
function from Σ to Z;
[[ - ]]assert maps each "assert" expression into a mathematical
function from Σ to B;
where Σ is a mathematical function from variables to Z.
- Reynolds Chapter 1 also serves as a review of familiar concepts
in predicate logic, e.g., what are logical inference rules and axioms, what
are formal proofs, what makes a logic sound, and what are bound and
free variables. If you want to learn more about formal logic,
please read the Chapters 1 and 2 of Huth and Ryan.
