3 ms·
Hah, the tidbit about Lamport having a different view from Hoare/Milner about revealing the control state is really spot-on. Coming from a mostly process-algeb
by lou1306 9y ago
Hah, the tidbit about Lamport having a different view from Hoare/Milner about revealing the control state is really spot-on.
Coming from a mostly process-algebra-oriented background (CSP, CCS and the like), TLA+ can sound both familiar and alien.
Thank you for the series!
- pron 9y agoAs I will discuss in part 4, the algebraic approach most similar to TLA is Ralph-Johan Back's and Joakim von Wright's refinement calculus/algebra. However, AFAIK, it doesn't (yet?) handle concurrent algorithms, whereas in TLA concurrent and sequential algorithms are formally indistinguishable (they are only distinguishable by how a reader informally interprets the formula; see the mention of "processes are in the eye of the beholder" in the post).