Go up to TopGo forward to Logic Versus Programming |

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

*Talking about concurrent algorithms!*

Author: Wolfgang Schreiner

Last Modification: May 14, 1998