# Semantics

## 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!$$