|
|
|---|
|
|
|
|---|
Dynamic semantics of Leo.
The dynamic semantics of Leo defines how the execution of the expressions, statements, etc. defined in the abstract syntax manipulate values and computation states.
The definition consists of mathematical structures that characterize the form of values and computation states, and functions saying how values and computation states are created and transformed by the execution of the Leo constructs. These execution functions do not assume that the constructs satisfy the static semantic requirements in thestatic semantics: the execution functions are defensive, i.e. they perform the dynamic equivalent of some of the static checks prescribed by the static semantics, such as the fact that an operator is applied to operands of the right types; if the checks fail, special error results are produced, distinct from values and computation states. An important property of Leo is that if the static semantic requirements in are satisfied, then these dynamic semantic checks never fail; we plan to formally prove this property.