Introduction to Semantics

• Semantics is about meaning: what do the expressions and statements of a programming language do? This is much more difficult than syntax, and formal methods for semantics have not been as widely used as EBNF in for syntax. In practice examples plus informal but carefully written English are often used to specify semantics.

  A few general categories of formal semantics have been tried:

  • Operational semantics defines the meaning of language by describing how it operates on a machine. One way to do this is to show how the language can be boiled down to a simpler intermediate language.

    For many programmers, operational semantics is a natural way to think about how programs work. When you try to understand what a language feature does by writing some test code for it, you are relying on an operational understanding of how it works,

  • Denotational semantics is a formal mathematical way of describing the meanings of programs. The basic idea is to associate mathematical objects with all the elements of a program, and then to specify meaning by using mathematical tools.

    See the first example of section 3.5.2.1 (binary numbers) to get an inkling of how it works.

  • Axiomatic semantics is a different mathematical approach to specifying meaning. Essentially, it uses logic to describe the meaning of code in a way that lets you prove that a program is correct (i.e. that it matches its specification). The book has a few sections on this technique, but we won’t get into it in this course.

• Informal English specifications are often used to describe the meanings of programming languages. For example, consider how Go defines if-statements. It uses EBNF for the syntax, and then plain English and one example for the semantics.

• As another example from Go, consider how it defines the panic (and recover) functions. Consider this:

  While executing a function F, an explicit call to panic or a run-time
  panic terminates the execution of F. Any functions deferred by F are then
  executed as usual. Next, any deferred functions run by F's caller are run,
  and so on up to any deferred by the top-level function in the executing
  goroutine. At that point, the program is terminated and the error
  condition is reported, including the value of the argument to panic. This
  termination sequence is called panicking.
  

  If you were writing a Go compiler, does this description tell you everything you need to know about the semantics of panic? One thing not explicitly described here is the order in which deferred functions are executed. Presumably, they are called in reverse order as described in the spec for defer. But this is not explicitly stated, and instead it must be inferred by the reader. The problem with being non-explicit is that two different readers might reasonably infer different things, and thus have different beliefs about what panic does.

• In contrast, the Scheme programming language manual comes with a complete formal denotational semantics. Scheme is an exceptionally simple language, but the semantics is a few pages of dense mathematics.