Go up to Top
Go forward to Logic Versus Programming
Talking about concurrent algorithms!
- Concurrent algorithm typically described by a program.
- Correctness of algorithm means program satisfies desired
- 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.
Id: tla1.tex,v 1.1 1996/04/29 08:36:08 schreine Exp schreine