Goals of a Programming Logic
Reasoning about concurrent algorithms.
- Simpler alternative to programming languages.
- No point in trading language for a complicated logic.
- Expressive to describe real algorithms.
- Formulas must not be too long and complicated to understand.
- TLA formulas:
- Familiar mathematical operators (and).
- ' (prime), always , exists .
- Combination of two logics:
- A logic of actions.
- A standard temporal logic.
Author: Wolfgang Schreiner
Last Modification: May 14, 1998