- Concurrent algorithm typically described by a program.
*Correctness*of algorithm means program satisfies desired property.

- TLA = Temporal Logic of Actions.
- Lamport, 1994.
- Both algorithm and property are specified by formulas in single logic.
- Correctness of algorithm means algorithm
*implies*property.

- Reasonable to abandon programing language?
- Mostly reasoning about concurrent algorithms.
- Concurrent programs are much to complicated.
- 1 page algorithm = 5000 lines of C code.
- Goal to detect algorithmic errors.

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine $$