Go backward to Refinement MappingsGo up to Top |

- TLA formulas describe algorithms:
- Effects of all statements.
- Control flow.
- Liveness properties.

- Advantages:
- Independent of language.
`All`information is explicitly specified in mathematical formulas.

- Problems:
- TLA formulas may get very large.
- Good structure and abstractions required to manage complexity.

Author: Wolfgang Schreiner

Last Modification: May 14, 1998