Go backward to Refinement Mappings Go up to Top

Summary

• 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.