Semantics

Semantics is the meaning of program phrases. We can distinguish two types of semantics:

• Static semantics: (context-sensitive) restriction of the set of valid program phrases; e.g., type systems.
  • Validation: testing that a program satisfies a property.
  • Documentation: documenting the meaning of a language.
  • Verification: proving that the programs of the language and/or the language itself satisfies a property.
• Dynamic semantics: run-time behavior of a program.

  • Operational semantics: the meaning of a phrase is given by an algorithm for reducing the phrase to a value.

  • Denotational semantics: the meaning of a phrase is this translation to an underlying mathematical domain.

    For example:

    

    Where Bin means the binary numbers. This $M$ is a recursive definition that maps a binary string to a natural number.

  • Axiomatic semantics: the meaning of a phrase is this set of axioms defining how it affects assertions about the program state.

    These semantics are more complex than the previous cases. A simple example is:

    

    This means that if x>3, and then we subtract 3 from x, then now x>0.

We will focus on operational semantics, as this corresponds to definitional interpreters.

Later in the course, we will add a Desugaring functionality (dynamically-typed):

And finally after that we will add a type checker to our language, to make sure that before interpreting our program will not crash (statically-typed):

As previously said, we want to build an interpreter. This is simply a method that, given a parsed expression ExprC, returns the corresponding Value:

Semantics is useful in various ways:

Interpretation vs Compilation

We distinguish:

• Interpreter: Directly performs the actions in the high level program.
• Compiler: Converts program to something executable by the platform.

Some differences between the two: