<p>There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into. </p>

<p>A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$. </p>

<p>Now, suppose we have two automata $(Q, q, f)$ and $(T, t, g)$. Let's ask a question: when are these automata equivalent? If all we are going to do is take the machines and send them inputs and listen to the outputs, we <em>don't</em> want to require the state sets to be the same (for example, if $(T, t, g)$ is the result of running a DFA minimization algorithm on $(Q, q, f)$). </p>

<p>It turns out that the right notion of equivalence is <em>bisimulation</em>.  The idea is that we take two state machines to be the same, if we can produce a relation $R \subseteq Q \times T$, such that </p>

<ul>
<li>$(q,t) \in R$</li>
<li>for all $(q,t) \in R$ and $i \in I$ and $o \in O$ then:
<ul>
<li>for all $q' \in Q$, if $(o, q') \in f(i, q)$, then there is a $t' \in T$ such that $(o, t') \in g(i, t)$. </li>
<li>for all $t' \in T$, if $(o, t') \in g(i, t)$, then there is a $q' \in Q$ such that $(o, q') \in f(i, q)$. </li>
</ul></li>
</ul>

<p>This says that if we can figure out any relation such that (a) the initial states are related, and (b) from related initial states, any I/O action the first machine can take can be mimicked by the second machine in a way that keeps you in the relation, and (c) similarly, the first machine can mimic anything the second can do.</p>

<p>Lamport's notation with primes is a way of concisely describing input-output relations. In this case, the state sets are the program counter of the first program, and the two program counters of the second program. The bisimulation relation is $R(pc, (p, c)) \triangleq pc = p \oplus c$, and then the bisimulation conditions follow trivially (since the relation expressions are equal under the subsitution). </p>

<p>The general theory at work is the theory of coinduction. State machines are representions of corecursively defined sets, and bisimulations tell you when two state machines are representations of the same potentially-infinite object. </p>

<p>Incidentally, this paper is written in a rather polemical style. Equally polemically, I'll point out that the style he advocates in this paper simply fails should you ever need to verify <em>part</em> of a program in isolation -- for example, if you want to prove a library implementation correct, or verifying a program using higher-order functions (or even just dynamic linking). </p>

<p>But both of us will use coinduction, nonetheless.</p>

CC BY-SA 3.0
2014-07-31T02:33:12.897Z
Thanks for your excellent answer. A quick search shows me that coinduction (which I know little) and bisimulation (which I know just a few) are themselves pretty big topics. Confusion about your *polemical* comment in the last but one paragraph: Which fails? Is it bisimulation? Isn't it popular in model checking and generally formal methods? I am not a native English speaker and am stumped on the inverted sentence. Would you mind explaining it in more details? Great thanks.
hengxin
CC BY-SA 3.0
2014-07-31T12:53:29.507Z
I have just learnt a little thing about *coinduction* from [this post](http://cs.stackexchange.com/a/528/4911): `Where inductive definitions build a structure from elementary building blocks, coinductive definitions shape structures from how they can be deconstructed`. I can get the basic idea. You claim that `State machines are representions of corecursively defined sets`. Why is it? Could you please make it more clear or provide some references? Thanks.
hengxin
CC BY-SA 3.0
2016-12-22T12:46:20.807Z
Lamport doesn't mention Milner because he developed his own theory  concurrently, starting in 1977. He doesn't need the concept of bisimulation because labeling *states* rather than events makes bisimulation coincide with the simpler, more convenient notion of trace-equivalence, and makes   LTL and FOL sufficient. Lamport's theory handles open specifications (libraries) elegantly, which he covered at length. In fact, any form of composition, including higher order, becomes simple conjunction in his formalism (not surprising as it's similar to ODEs, just discrete and designed for refinements).
pron
CC BY-SA 3.0
2016-12-27T17:33:12.040Z
@pron: No, Lamport's formalism doesn't handle libraries adequately. Try working out what the spec of a memory allocator or thread scheduler should be, bearing in mind it has to run in the same address space as client code. (It's not enough to treat these as primitive abstractions because the same patterns show up at higher levels of the stack -- eg, connection pooling for DB access is morally the same as a malloc implementation, and GUI libraries basically implement threading abstractions.)
Neel Krishnaswami
CC BY-SA 3.0
2016-12-27T18:17:38.730Z
@NeelKrishnaswami I don't see any problem, but perhaps you could pinpoint the issue. It was Lamport who proved the soundness of assume-guarantee proofs for concurrent systems (w/parallel composition), and those are well-handled by his formalism. See https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-conjoining.pdf and/or https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-open.pdf
pron
CC BY-SA 3.0
2017-01-18T10:34:58.070Z
@pron: the main problems in Lamport's approach (which I gloss as "just use LTL") is the fact that its treatment of state is too weak/naive, particularly the lack of good proof techniques for handling dynamic allocation, higher-order state, and separation/aliasing. Some good examples: (a) proofs involving locks storable in the heap, (b) program specs which are invariant under gc, and (c) giving a spec for the implementation of an event loop.
Neel Krishnaswami
CC BY-SA 3.0
2017-01-18T10:37:53.843Z
@pron: (continued) E.g., Lamport's specification language PlusCal for TLA+ only supports pure first-order state, and if there are nontrivial pointer manipulations you have to code up a fake heap manually. (C.f. his paper * Checking a Multithreaded Algorithm with +CAL*, which works around these issues in an ad-hoc way.) If all you care about is verifying high-level algorithms in isolation, his approach is okay, but if we want to do proofs of the actual programs we run, we have to understand the semantics of the actual code.
Neel Krishnaswami
CC BY-SA 3.0
2017-01-18T18:32:14.203Z
@NeelKrishnaswami I did separation in TLA+ in a matter of hours, as a beginner. Sure, "simulated heap", but so what? Your claim is really: "it's hard to do end-to-end in TLA+". That's not a problem, though, but a feature, with very distinctive pros and cons, and Lamport has very convincing arguments as to why this approach is relevant in many more cases than end-to-end (and is *far* cheaper). He invented TLA+ as a *counterpoint* to work in semantics.
pron
CC BY-SA 3.0
2017-01-18T18:37:09.750Z
@NeelKrishnaswami Also, TLA+ is very, very far from being "just use LTL". In fact, Lamport writes in one of the TLA+ docs that, and I quote, "temporal logic is evil", and TLA tries to avoid it as much as possible (it's really used almost only for liveness). Sure, TLA doesn't answer all problems, but in sacrificing modeling programming languages, it has come closer to being the purest, most elegant, and simplest mathematical formulation of computation (and in particular, refinement) than any other approach I've seen. It has also proven itself to be of great pragmatic value in the field.
pron
CC BY-SA 3.0
2017-01-19T11:42:39.890Z
@pron: No, my real claim is just what I said it is: the treatment of state is too weak. Of course, it's a consequence of this weakness that you can't do end-to-end verification, since machine code is a higher-order stateful language, but none of the examples I suggested involve an end-to-end property. (And indeed, the original Reynolds-style formulation of separation you allude to can't handle them well either.)
Neel Krishnaswami
CC BY-SA 3.0
2017-01-19T11:50:48.887Z
@pron: Now, you should definitely use refinement whenever you can, but  1) since it's a monotonicity property, it doesn't work well when in the presence of higher-order constructions, and 2) many programs involve higher-order constructions. When you do give good specifications for higher-order constructs, they end up looking like realizability models. The mathematics of formal semantics is inevitable. While you can put your head in the sand about it, you can also take advantage of it and look for presentations of those algebraic structures. We call those presentations "programming languages"!
Neel Krishnaswami
CC BY-SA 3.0
2017-01-19T20:56:30.570Z
@NeelKrishnaswami 1) I need to see examples of what you mean b/c TLA+ is far more higher-order than PL people think (due to modules and interesting compositions), but, more importantly, 2) this is exactly the kind of thinking that TLA was built to avoid. TLA+ is not intended to model other *formalisms*. I have nothing against exploring PL semantics (unlike Lamport), but I think that TLA+ is a radical alternative with some very promising results. A *program* may have higher order constructions that the *algorithm* it specifies does not. TLA+ specifies algorithms and systems, not programs.
pron
CC BY-SA 3.0
2017-01-19T20:58:22.803Z
@NeelKrishnaswami Lamport writes: "Proponents of formalism A often claim that formalism B is inadequate because concepts that are fundamental to specifications written with A cannot be expressed with B. Such arguments are misleading. The purpose of a formalism is not to express specifications written in another formalism, but to specify some aspects of some class of computer systems. Specifications of the same system written with two different formalisms are likely to be formally incomparable."
pron
CC BY-SA 3.0
2017-01-20T10:50:31.357Z
@NeelKrishnaswami Also, you can do end-to-end in TLA+ (http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf), it's just not really what it's for. If you want to abuse TLA, you could express any program in any programming language (imperative, functional, declarative, p-calc), including machine code, as a TLA formula F = **∃** hiddenState : ◻(F1 ∧ ... ∧ Fn), where F1...Fn are the subexpression of the program and recursively take the same form (**∃** is temporal existential quantification). The composition may be sequential, parallel, application, or declarative rules.
pron
CC BY-SA 3.0
2017-01-20T11:25:45.790Z
@pron: A computer gives you a global memory, and since systems have to be built from components, the component specifications must explain how to share that global state without knowing what the other components even are. Full support for functions makes this issue impossible to avoid, since you have to be able to call a function without knowing its code and execute the body without knowing the evaluation context, but similar issues arise over and over at every level of the software stack. That's what makes checking the treatment of higher-order state a good diagnostic.
Neel Krishnaswami
CC BY-SA 3.0
2017-01-20T11:43:40.033Z
@pron: For examples, see Svendsen and Birkedal's paper *Impredicative Concurrent Abstract Predicates*, particularly the specs for storable locks and event loops. Note that (a) the specs are very simple, (b) you could translate their model construction into the TLA spec language, but if you did, (c) you would die of old age before instantiating all the resulting quantifiers in any realistic proof.
Neel Krishnaswami
CC BY-SA 3.0
2017-01-20T21:40:35.607Z
@NeelKrishnaswami Ah, good example. At first glance, I *believe* that it poses no problem in TLA+, as you can parameterize the lock module over propositions R, with some natural modeling of program state that is both useful and simple in practice. Parameterization + nondeterminism (which is how TLA+ models types; in TLA "types" and programs can not only make use of the same syntactic terms, as with dependent types, but are actually the same kind of object) makes this possible. If you don't mind, we can continue this discussion over email, and I'll show you what I have in mind.
pron
CC BY-SA 3.0
2014-07-30T11:02:56.983Z
2014-07-30T11:02:56.983Z
Neel Krishnaswami
<p>The short paper <a href="http://research.microsoft.com/en-us/um/people/lamport/pubs/deroever-festschrift.pdf" rel="nofollow">"Computer Science and State Machines"</a> by Leslie Lamport seems quite strange to me.<br>
On the one hand, I am surprised to see that an important hardware protocol called "two-phase handshake" can be derived from a trivial program, simply by <strong>mathematical substitution</strong>.<br>
On the other hand, I think that this example is (and <em>should be</em>) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples.</p>

<p><strong>My question is straightforward:</strong></p>

<blockquote>
  <p>Is this derivation a coincidence? Could anyone offer more examples or related references?</p>
</blockquote>

<hr>

<p><strong>The derivation of the "two-phase handshake" protocol from a trivial program:</strong></p>

<p>The trivial program mentioned above is just to alternately perform the $\mathcal{P}$ and $\mathcal{C}$ operations:</p>

<blockquote>
  <p>$\mathcal{X}: \textrm{ loop } \mathcal{P} \textrm{ } ; \textrm{ } \mathcal{C} \textrm{ endloop}$</p>
</blockquote>

<p>By introducing a variable $pc$ to represent the "program counter", $\mathcal{X}$ can be described as the following state machine:</p>

<blockquote>
  <ul>
  <li>$Init_{\mathcal{X}} \triangleq (pc = 0) \land Init_{\mathcal{PC}}$</li>
  <li>$Next_{\mathcal{X}} \triangleq \big( (pc = 0) \land \mathcal{P} \land (pc' = 1) \big) \lor \big( (pc = 1) \land \mathcal{C} \land (pc' = 0) \big)$</li>
  </ul>
</blockquote>

<p>where $Init_{\mathcal{X}}$ denotes the set of initial states; $Next_{\mathcal{X}}$ specifies the next-step transition. $Init_{\mathcal{PC}}$ specifies the initial values of the variables in $var_{\mathcal{PC}}$ involved in $\mathcal{P}$ and $\mathcal{C}$. The primed variable ($pc'$ here) is used to represent the modified version of its unprimed counterpart ($pc$ here).</p>

<p>The two-phase handshake protocol can be described as follows, where $p$ and $c$ are initially equal.</p>

<blockquote>
  <p>\begin{eqnarray}
\mathcal{Y} :  &amp; \textrm{ process } &amp; Prod: \textrm{ whenever } p = c \textrm{ do } \mathcal{P} \textrm{ } ; \textrm{ } p = p \oplus 1 \textrm{ end} \\
&amp; \Arrowvert &amp; \\
&amp; \textrm{ process } &amp; Cons: \textrm{ whenever } p \neq c \textrm{ do } \mathcal{C} \textrm{ } ; \textrm{ } c = c \oplus 1 \textrm{ end}
\end{eqnarray}</p>
</blockquote>

<p>Note that process $Prod$ reads $c$ and writes $p$ while $Cons$ reads $p$ and writes $c$. It is not hard to find out that $\mathcal{Y}$ alternately performs $\mathcal{P}$ and $\mathcal{C}$.</p>

<p>The protocol $\mathcal{Y}$ can also be described as a state machine:</p>

<blockquote>
  <ul>
  <li>$Init_{\mathcal{Y}} \triangleq (p = c) \land Init_{\mathcal{PC}}$</li>
  <li>$Next_{\mathcal{Y}} \triangleq Prod \lor Cons$</li>
  <li>$Prod \triangleq (p = c) \land \mathcal{P} \land (p' = p \oplus 1) \land (c' = c)$</li>
  <li>$Cons \triangleq (p \neq c) \land \mathcal{C} \land (c' = c \oplus 1) \land (p' = p)$</li>
  </ul>
</blockquote>

<p>The amazing observation is:</p>

<blockquote>
  <p>$\mathcal{Y}$ can be obtained from $\mathcal{X}$ by substituting $p \oplus c$ for $pc$ in their state machines.</p>
</blockquote>

CC BY-SA 3.0
2014-07-25T23:20:30.360Z
This is a great question.  But I have one small comment on it.  You write: *"I doubt that this lovely derivation has been chosen deliberately."* - I'm not sure what you were getting at here.  I have no problem believing that Lamport deliberately chose this example to illustrate his point in the best way he was able.  I'm not sure how that relates to your ultimate question anyway.
D.W.
CC BY-SA 3.0
2014-07-26T01:31:43.620Z
@D.W. Thanks for your comment. I also believe that this example is (and *should be*) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples. (updated the post)
hengxin
CC BY-SA 3.0
2014-07-30T06:12:45.460Z
In order to get some intuition, it might be helpful to see where it gets by considering all 16 boolean functions on two boolean variables p and c.
Abel Molina
<reference-request><pl.programming-languages><formal-methods><examples>
Describing state machines mathematically
hengxin
# Describing state machines mathematically

(Asked by: username_0 on 2014-07-25)

The short paper ["Computer Science and State Machines"](http://research.microsoft.com/en-us/um/people/lamport/pubs/deroever-festschrift.pdf) by Leslie Lamport seems quite strange to me.  
On the one hand, I am surprised to see that an important hardware protocol called "two-phase handshake" can be derived from a trivial program, simply by **mathematical substitution**.  
On the other hand, I think that this example is (and *should be*) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples.

**My question is straightforward:**

> Is this derivation a coincidence? Could anyone offer more examples or related references?

---

**The derivation of the "two-phase handshake" protocol from a trivial program:**

The trivial program mentioned above is just to alternately perform the $\mathcal{P}$ and $\mathcal{C}$ operations:

> $\mathcal{X}: \textrm{ loop } \mathcal{P} \textrm{ } ; \textrm{ } \mathcal{C} \textrm{ endloop}$

By introducing a variable $pc$ to represent the "program counter", $\mathcal{X}$ can be described as the following state machine:

> * $Init\_{\mathcal{X}} \triangleq (pc = 0) \land Init\_{\mathcal{PC}}$
> * $Next\_{\mathcal{X}} \triangleq \big( (pc = 0) \land \mathcal{P} \land (pc' = 1) \big) \lor \big( (pc = 1) \land \mathcal{C} \land (pc' = 0) \big)$

where $Init\_{\mathcal{X}}$ denotes the set of initial states; $Next\_{\mathcal{X}}$ specifies the next-step transition. $Init\_{\mathcal{PC}}$ specifies the initial values of the variables in $var\_{\mathcal{PC}}$ involved in $\mathcal{P}$ and $\mathcal{C}$. The primed variable ($pc'$ here) is used to represent the modified version of its unprimed counterpart ($pc$ here).

The two-phase handshake protocol can be described as follows, where $p$ and $c$ are initially equal.

> \begin{eqnarray}
> \mathcal{Y} : & \textrm{ process } & Prod: \textrm{ whenever } p = c \textrm{ do } \mathcal{P} \textrm{ } ; \textrm{ } p = p \oplus 1 \textrm{ end} \\
> & \Arrowvert & \\
> & \textrm{ process } & Cons: \textrm{ whenever } p \neq c \textrm{ do } \mathcal{C} \textrm{ } ; \textrm{ } c = c \oplus 1 \textrm{ end}
> \end{eqnarray}

Note that process $Prod$ reads $c$ and writes $p$ while $Cons$ reads $p$ and writes $c$. It is not hard to find out that $\mathcal{Y}$ alternately performs $\mathcal{P}$ and $\mathcal{C}$.

The protocol $\mathcal{Y}$ can also be described as a state machine:

> * $Init\_{\mathcal{Y}} \triangleq (p = c) \land Init\_{\mathcal{PC}}$
> * $Next\_{\mathcal{Y}} \triangleq Prod \lor Cons$
> * $Prod \triangleq (p = c) \land \mathcal{P} \land (p' = p \oplus 1) \land (c' = c)$
> * $Cons \triangleq (p \neq c) \land \mathcal{C} \land (c' = c \oplus 1) \land (p' = p)$

The amazing observation is:

> $\mathcal{Y}$ can be obtained from $\mathcal{X}$ by substituting $p \oplus c$ for $pc$ in their state machines.

**Tags:** reference-request, pl.programming-languages, formal-methods, examples
> **Comments:**
> **username_1**: This is a great question.  But I have one small comment on it.  You write: *"I doubt that this lovely derivation has been chosen deliberately."* - I'm not sure what you were getting at here.  I have no problem believing that Lamport deliberately chose this example to illustrate his point in the best way he was able.  I'm not sure how that relates to your ultimate question anyway.  
> **username_0**: @D.W. Thanks for your comment. I also believe that this example is (and *should be*) chosen deliberately. What I doubt about is its generality. If this method (i.e., describing state machines mathematically and deriving a protocol from its specification by mathematical substitution) is so fresh that researchers have not developed a general theory, I would like to see more examples. (updated the post)  
> **username_2**: In order to get some intuition, it might be helpful to see where it gets by considering all 16 boolean functions on two boolean variables p and c.  

---

## 1 answers

### Answer by username_3 on 2014-07-30. Score: 7 | Accepted answer

There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into.

A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$.

Now, suppose we have two automata $(Q, q, f)$ and $(T, t, g)$. Let's ask a question: when are these automata equivalent? If all we are going to do is take the machines and send them inputs and listen to the outputs, we *don't* want to require the state sets to be the same (for example, if $(T, t, g)$ is the result of running a DFA minimization algorithm on $(Q, q, f)$).

It turns out that the right notion of equivalence is *bisimulation*. The idea is that we take two state machines to be the same, if we can produce a relation $R \subseteq Q \times T$, such that

* $(q,t) \in R$
* for all $(q,t) \in R$ and $i \in I$ and $o \in O$ then:
  + for all $q' \in Q$, if $(o, q') \in f(i, q)$, then there is a $t' \in T$ such that $(o, t') \in g(i, t)$.
  + for all $t' \in T$, if $(o, t') \in g(i, t)$, then there is a $q' \in Q$ such that $(o, q') \in f(i, q)$.

This says that if we can figure out any relation such that (a) the initial states are related, and (b) from related initial states, any I/O action the first machine can take can be mimicked by the second machine in a way that keeps you in the relation, and (c) similarly, the first machine can mimic anything the second can do.

Lamport's notation with primes is a way of concisely describing input-output relations. In this case, the state sets are the program counter of the first program, and the two program counters of the second program. The bisimulation relation is $R(pc, (p, c)) \triangleq pc = p \oplus c$, and then the bisimulation conditions follow trivially (since the relation expressions are equal under the subsitution).

The general theory at work is the theory of coinduction. State machines are representions of corecursively defined sets, and bisimulations tell you when two state machines are representations of the same potentially-infinite object.

Incidentally, this paper is written in a rather polemical style. Equally polemically, I'll point out that the style he advocates in this paper simply fails should you ever need to verify *part* of a program in isolation -- for example, if you want to prove a library implementation correct, or verifying a program using higher-order functions (or even just dynamic linking).

But both of us will use coinduction, nonetheless.

> **Comments:**
> **username_0**: Thanks for your excellent answer. A quick search shows me that coinduction (which I know little) and bisimulation (which I know just a few) are themselves pretty big topics. Confusion about your *polemical* comment in the last but one paragraph: Which fails? Is it bisimulation? Isn't it popular in model checking and generally formal methods? I am not a native English speaker and am stumped on the inverted sentence. Would you mind explaining it in more details? Great thanks.  
> **username_0**: I have just learnt a little thing about *coinduction* from [this post](http://cs.stackexchange.com/a/528/4911): `Where inductive definitions build a structure from elementary building blocks, coinductive definitions shape structures from how they can be deconstructed`. I can get the basic idea. You claim that `State machines are representions of corecursively defined sets`. Why is it? Could you please make it more clear or provide some references? Thanks.  
> **username_4**: Lamport doesn't mention Milner because he developed his own theory  concurrently, starting in 1977. He doesn't need the concept of bisimulation because labeling *states* rather than events makes bisimulation coincide with the simpler, more convenient notion of trace-equivalence, and makes   LTL and FOL sufficient. Lamport's theory handles open specifications (libraries) elegantly, which he covered at length. In fact, any form of composition, including higher order, becomes simple conjunction in his formalism (not surprising as it's similar to ODEs, just discrete and designed for refinements).  
> **username_3**: @pron: No, Lamport's formalism doesn't handle libraries adequately. Try working out what the spec of a memory allocator or thread scheduler should be, bearing in mind it has to run in the same address space as client code. (It's not enough to treat these as primitive abstractions because the same patterns show up at higher levels of the stack -- eg, connection pooling for DB access is morally the same as a malloc implementation, and GUI libraries basically implement threading abstractions.)  
> **username_4**: @NeelKrishnaswami I don't see any problem, but perhaps you could pinpoint the issue. It was Lamport who proved the soundness of assume-guarantee proofs for concurrent systems (w/parallel composition), and those are well-handled by his formalism. See https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-conjoining.pdf and/or https://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-open.pdf  
> **username_3**: @pron: the main problems in Lamport's approach (which I gloss as "just use LTL") is the fact that its treatment of state is too weak/naive, particularly the lack of good proof techniques for handling dynamic allocation, higher-order state, and separation/aliasing. Some good examples: (a) proofs involving locks storable in the heap, (b) program specs which are invariant under gc, and (c) giving a spec for the implementation of an event loop.  
> **username_3**: @pron: (continued) E.g., Lamport's specification language PlusCal for TLA+ only supports pure first-order state, and if there are nontrivial pointer manipulations you have to code up a fake heap manually. (C.f. his paper * Checking a Multithreaded Algorithm with +CAL*, which works around these issues in an ad-hoc way.) If all you care about is verifying high-level algorithms in isolation, his approach is okay, but if we want to do proofs of the actual programs we run, we have to understand the semantics of the actual code.  
> **username_4**: @NeelKrishnaswami I did separation in TLA+ in a matter of hours, as a beginner. Sure, "simulated heap", but so what? Your claim is really: "it's hard to do end-to-end in TLA+". That's not a problem, though, but a feature, with very distinctive pros and cons, and Lamport has very convincing arguments as to why this approach is relevant in many more cases than end-to-end (and is *far* cheaper). He invented TLA+ as a *counterpoint* to work in semantics.  
> **username_4**: @NeelKrishnaswami Also, TLA+ is very, very far from being "just use LTL". In fact, Lamport writes in one of the TLA+ docs that, and I quote, "temporal logic is evil", and TLA tries to avoid it as much as possible (it's really used almost only for liveness). Sure, TLA doesn't answer all problems, but in sacrificing modeling programming languages, it has come closer to being the purest, most elegant, and simplest mathematical formulation of computation (and in particular, refinement) than any other approach I've seen. It has also proven itself to be of great pragmatic value in the field.  
> **username_3**: @pron: No, my real claim is just what I said it is: the treatment of state is too weak. Of course, it's a consequence of this weakness that you can't do end-to-end verification, since machine code is a higher-order stateful language, but none of the examples I suggested involve an end-to-end property. (And indeed, the original Reynolds-style formulation of separation you allude to can't handle them well either.)  
> **username_3**: @pron: Now, you should definitely use refinement whenever you can, but  1) since it's a monotonicity property, it doesn't work well when in the presence of higher-order constructions, and 2) many programs involve higher-order constructions. When you do give good specifications for higher-order constructs, they end up looking like realizability models. The mathematics of formal semantics is inevitable. While you can put your head in the sand about it, you can also take advantage of it and look for presentations of those algebraic structures. We call those presentations "programming languages"!  
> **username_4**: @NeelKrishnaswami 1) I need to see examples of what you mean b/c TLA+ is far more higher-order than PL people think (due to modules and interesting compositions), but, more importantly, 2) this is exactly the kind of thinking that TLA was built to avoid. TLA+ is not intended to model other *formalisms*. I have nothing against exploring PL semantics (unlike Lamport), but I think that TLA+ is a radical alternative with some very promising results. A *program* may have higher order constructions that the *algorithm* it specifies does not. TLA+ specifies algorithms and systems, not programs.  
> **username_4**: @NeelKrishnaswami Lamport writes: "Proponents of formalism A often claim that formalism B is inadequate because concepts that are fundamental to specifications written with A cannot be expressed with B. Such arguments are misleading. The purpose of a formalism is not to express specifications written in another formalism, but to specify some aspects of some class of computer systems. Specifications of the same system written with two different formalisms are likely to be formally incomparable."  
> **username_4**: @NeelKrishnaswami Also, you can do end-to-end in TLA+ (http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf), it's just not really what it's for. If you want to abuse TLA, you could express any program in any programming language (imperative, functional, declarative, p-calc), including machine code, as a TLA formula F = **∃** hiddenState : ◻(F1 ∧ ... ∧ Fn), where F1...Fn are the subexpression of the program and recursively take the same form (**∃** is temporal existential quantification). The composition may be sequential, parallel, application, or declarative rules.  
> **username_3**: @pron: A computer gives you a global memory, and since systems have to be built from components, the component specifications must explain how to share that global state without knowing what the other components even are. Full support for functions makes this issue impossible to avoid, since you have to be able to call a function without knowing its code and execute the body without knowing the evaluation context, but similar issues arise over and over at every level of the software stack. That's what makes checking the treatment of higher-order state a good diagnostic.  
> **username_3**: @pron: For examples, see Svendsen and Birkedal's paper *Impredicative Concurrent Abstract Predicates*, particularly the specs for storable locks and event loops. Note that (a) the specs are very simple, (b) you could translate their model construction into the TLA spec language, but if you did, (c) you would die of old age before instantiating all the resulting quantifiers in any realistic proof.  
> **username_4**: @NeelKrishnaswami Ah, good example. At first glance, I *believe* that it poses no problem in TLA+, as you can parameterize the lock module over propositions R, with some natural modeling of program state that is both useful and simple in practice. Parameterization + nondeterminism (which is how TLA+ models types; in TLA "types" and programs can not only make use of the same syntactic terms, as with dependent types, but are actually the same kind of object) makes this possible. If you don't mind, we can continue this discussion over email, and I'll show you what I have in mind.  

---

