Why formalize semantics?

  • Standardizes the official semantics of the language
    • This is important for compilers; otherwise you end up with multiple compilers where programs might behave differently
  • Allows for a formal analysis of the properties of the language
  • An implementation of the language can be derived from the semantics specification (Reference)
  • There is no uniformal way to specify language semantics
    • It is harder to do than formally specifying syntax (unlike with BNF etc)
  • Semantic definition methods fall into three groups:

Operational Semantics

  • The meaning of a well-formed program is the trace of computation steps that result from processing the program’s input
  • Also called intensional semantics, because the sequence of internal computation steps (the “intension”) is the most important
  • Two differently coded programs that both compute factorial have different operational semantics

Denotational Semantics

  • The meaning of a well-formed program is a mathematical function from input data to output data
  • The exact steps that are taken to form the output are irrelevant
  • The relation between input to output is the thing, that matters
  • Also called extensional semantics
  • Here the two differently coded factorial programs have the same denotational semantics

Axiomatic Semantics

  • The meaning of a well-formed program is a logical proposition (specification) that states properties about input and output
  • The axiomatic semantics of the factorial program are described by \(\forall x. x \geq 0 \Rightarrow \exists y. y = x!\)