4 ms·

Formal specs as sets of behaviors

56 points by gm678 1y ago

AndrewKemendo 1y ago
There’s definitely some good patterns in here. Needs worked examples
thdhhghgbhy 1y ago
I was hoping for a TLA+ example, but it never got there.
- ethan_smith 1y ago
  Hillel Wayne's "Practical TLA+" book and the TLA+ examples repository (https://github.com/tlaplus/Examples https://github.com/tlaplus/Examples) both contain excellent worked examples ranging from simple algorithms to complex distributed systems.
  - thdhhghgbhy 1y ago
    Thanks. Tangentially TLA+ seems to be most useful for finding concurrency bugs. I'm yet to find a compelling example of it used for a fairly mundane, by that I mean composed of mainly sequential processes, systems architecture.
csb6 1y ago
As a counterpoint, Dijkstra [0] makes a distinction between what he calls “postulational” and “operational” (more like what TFA is describing) formal methods. (Sidenote: I think people nowadays would use “denotational” instead of “postulational” (e.g. denotational vs. operational semantics), but Dijkstra wrote this in the 1980s) Instead of thinking of a program as a set of potential execution traces, he advocated thinking of programs as formulas (e.g. pre/postconditions) that can be used to construct proofs without having to simulate any executions. His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs. I am just an amateur but it seems like formal methods as a whole is often conflated with model checking and other operational formal methods. [0] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1012.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD101...
- mrtesthah 1y ago
  >His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs. I love the idea. Are you aware of any such spec-based code generators in widespread use today?
  - csb6 1y ago
    The most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several driverless train control systems in the Paris Metro and other subways. There is a free version but unfortunately it is not open source. [0] https://www.atelierb.eu/en/ https://www.atelierb.eu/en/
- pron 1y ago
  While there is a proof assistant for checking TLA+ proofs and a couple of model checkers for subsets of TLA+, TLA+ itself is no more and no less than a formal language for expressing mathematical formulas that describe dynamical systems. There is no notion of code, program, or execution in TLA+ any more than the formula y(t) = y0 + v0t - 0.5gt^2 has the notion of a ball, a vacuum, or of Earth. When the author talks about "sets of behaviours" (really, classes of behaviours, but that's getting too technical) it is precisely in the same sense that the formula `x > 3` denotes the set of all integers > 3 in a logic over the integers. What's interesting about TLA+ (or, really, about TLA, the temporal logic at the core of TLA+) is how change over time is represented. Rather than with an explicit time variable, TLA intrinsically represents the evolution of the values of variables over time in a way that makes abstraction-refinement relations (the relation between more and less detailed descriptions of a dynamical system) particularly easy to express. Dijkstra's pre/post conditions can be expressed in TLA+ just as anything that could be stated precisely could be expressed in any sufficiently rich mathematical language. We can choose to interpret some TLA+ formulas as "programs" just as we can choose to interpret some formulas as describing the motion of a baseball in a vacuum, but TLA+ allows us to express things that are more abstract than programs, which can be very useful (e.g. no program can express the Quicksort algorithm in its full generality, as that algorithm is too abstract to be a program, but it is nevertheless very useful to show that a particular program is a particular implementation of that algorithm).
pron 1y ago
> there have been a number of formal specification tools that have been developed in recent years which use programming-language-like notation, such as FizzBee, P, PlusCal, and Quint. I think these notations are more approachable for programmers than the more set-theoretic notation of TLA+. This statement may make it seem like the design of those other languages is a later development than TLA+, while the opposite is the case. Programming-language-like specification languages have existed continuously since the 70s and 80s (VDM, Estelle, SMV, Spin/PROMELLA - they were about as known to practising programmers at the time as the newer ones are known today...), as well as model-checkable programming languages similar to P (Esterel). The new incarnations are very similar to those from more than four decades ago. TLA+ was the newer development, designed as a reaction to the old programming-like approach, which, Leslie Lamport felt, wasn't simple and succinct enough, didn't allow for specification at arbitrary levels of detail, and didn't allow for easy manipulation and substitution (e.g. that `x = 2` might mean something different from `x + 3 = 5` is not just added complexity, but makes it hard to describe the relationship between specifications of the same system at different levels of detail). Lamport decided to ditch the older style in favour of one based almost solely on simple mathematics (there were some earlier attempts, but they were still more programming-like than TLA+). He didn't expect that mathematics at the level taught in an introductory, first-semester university course would be so unapproachable to programmers.
- 082349872349872 1y ago
  Wetware programmers may have found the mathematics unapproachable, but what about the LLMs?
- jackdaniels4me 1y ago
  Lamport didn't design TLA+ for model checking or for practicing developers to use. He did purely for publishing papers where the researchers express their proofs as math (his new TLA+) instead of free form text.
  - pron 1y ago
    TLA+ was specifically designed for practitioners (https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html), although he did use earlier incarnations of TLA to analyse his own concurrent and distributed algorithms. His paper explaining TLA [1] says: > We are motivated not by an abstract ideal of elegance, but by the practical problem of reasoning about real algorithms. Rigorous reasoning is the only way to avoid subtle errors in concurrent algorithms, and we want to make reasoning as simple as possible by making the underlying formalism simple. The introduction to the book says: > TLA provides a mathematical foundation for describing systems. To write specifications, we need a complete language built atop that foundation. I ini- tially thought that this language should be some sort of abstract programming language whose semantics would be based on TLA. I didn’t know what kind of programming language constructs would be best, so I decided to start writing specifications directly in TLA. I intended to introduce programming constructs as I needed them. To my surprise, I discovered that I didn’t need them. What I needed was a robust language for writing mathematics. > Although mathematicians have developed the science of writing formulas, they haven’t turned that science into an engineering discipline. ... The specification of a real system can be dozens or even hundreds of pages long. Mathematicians know how to write 20-line formulas, not 20-page formulas. So, I had to introduce notations for writing long formulas. What I took from programming languages were ideas for modularizing large specifications. And the Getting Started portion says: > A system specification consists of a lot of ordinary mathematics glued together with a tiny bit of temporal logic. That’s why most TLA+ constructs are for expressing ordinary mathematics. To write specifications, you have to be familiar with this ordinary math. Unfortunately, the computer science departments in many universities apparently believe that fluency in C++ is more important than a sound education in elementary mathematics. So, some readers may be unfamiliar with the math needed to write specifications. Fortunately, this math is quite simple. If exposure to C++ hasn’t destroyed your ability to think logically, you should have no trouble filling any gaps in your mathematics education. He recognises the tradeoffs of abandoning the programming style, but it is done to make the language simple and practitioner-friendly (and it is a much simpler language than Python, let alone any other specification language, all while preserving maximal expressive power). You can have an opinion on whether this is a good tradeoff or not, but it was done intentionally, and with the purpose of helping practitioners. [1]: https://lamport.azurewebsites.net/pubs/lamport-actions.pdf https://lamport.azurewebsites.net/pubs/lamport-actions.pdf
deterministic 1y ago
Transactional vs. Reactive systems is not a good way to think about it IMHO. A "Reactive system" is basically a "Transactional system" that in addition takes a system state as input and returns a (updated) system state as output: reactive_system : (State * Input) -> (State * Output) Which makes it identical (from a formal point of view) to a "Transactional system".

56 points by gm678 1y ago

AndrewKemendo 1y ago

There’s definitely some good patterns in here. Needs worked examples

thdhhghgbhy 1y ago

I was hoping for a TLA+ example, but it never got there.

ethan_smith 1y ago
Hillel Wayne's "Practical TLA+" book and the TLA+ examples repository (https://github.com/tlaplus/Examples https://github.com/tlaplus/Examples) both contain excellent worked examples ranging from simple algorithms to complex distributed systems.
- thdhhghgbhy 1y ago
  Thanks. Tangentially TLA+ seems to be most useful for finding concurrency bugs. I'm yet to find a compelling example of it used for a fairly mundane, by that I mean composed of mainly sequential processes, systems architecture.

csb6 1y ago

As a counterpoint, Dijkstra [0] makes a distinction between what he calls “postulational” and “operational” (more like what TFA is describing) formal methods. (Sidenote: I think people nowadays would use “denotational” instead of “postulational” (e.g. denotational vs. operational semantics), but Dijkstra wrote this in the 1980s) Instead of thinking of a program as a set of potential execution traces, he advocated thinking of programs as formulas (e.g. pre/postconditions) that can be used to construct proofs without having to simulate any executions. His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs. I am just an amateur but it seems like formal methods as a whole is often conflated with model checking and other operational formal methods. [0] https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1012.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD101...

mrtesthah 1y ago
>His idea with weakest preconditions was to derive code from the desired logical properties, not to prove that a priori written code satisfies those properties, reckoning that his way would be less work and result in more elegant programs. I love the idea. Are you aware of any such spec-based code generators in widespread use today?
- csb6 1y ago
  The most developed one I know of is Atelier B [0], which uses the B-Method and has a C code generator. I believe this was the tool used to develop several driverless train control systems in the Paris Metro and other subways. There is a free version but unfortunately it is not open source. [0] https://www.atelierb.eu/en/ https://www.atelierb.eu/en/
pron 1y ago
While there is a proof assistant for checking TLA+ proofs and a couple of model checkers for subsets of TLA+, TLA+ itself is no more and no less than a formal language for expressing mathematical formulas that describe dynamical systems. There is no notion of code, program, or execution in TLA+ any more than the formula y(t) = y0 + v0t - 0.5gt^2 has the notion of a ball, a vacuum, or of Earth. When the author talks about "sets of behaviours" (really, classes of behaviours, but that's getting too technical) it is precisely in the same sense that the formula `x > 3` denotes the set of all integers > 3 in a logic over the integers. What's interesting about TLA+ (or, really, about TLA, the temporal logic at the core of TLA+) is how change over time is represented. Rather than with an explicit time variable, TLA intrinsically represents the evolution of the values of variables over time in a way that makes abstraction-refinement relations (the relation between more and less detailed descriptions of a dynamical system) particularly easy to express. Dijkstra's pre/post conditions can be expressed in TLA+ just as anything that could be stated precisely could be expressed in any sufficiently rich mathematical language. We can choose to interpret some TLA+ formulas as "programs" just as we can choose to interpret some formulas as describing the motion of a baseball in a vacuum, but TLA+ allows us to express things that are more abstract than programs, which can be very useful (e.g. no program can express the Quicksort algorithm in its full generality, as that algorithm is too abstract to be a program, but it is nevertheless very useful to show that a particular program is a particular implementation of that algorithm).

pron 1y ago

> there have been a number of formal specification tools that have been developed in recent years which use programming-language-like notation, such as FizzBee, P, PlusCal, and Quint. I think these notations are more approachable for programmers than the more set-theoretic notation of TLA+. This statement may make it seem like the design of those other languages is a later development than TLA+, while the opposite is the case. Programming-language-like specification languages have existed continuously since the 70s and 80s (VDM, Estelle, SMV, Spin/PROMELLA - they were about as known to practising programmers at the time as the newer ones are known today...), as well as model-checkable programming languages similar to P (Esterel). The new incarnations are very similar to those from more than four decades ago. TLA+ was the newer development, designed as a reaction to the old programming-like approach, which, Leslie Lamport felt, wasn't simple and succinct enough, didn't allow for specification at arbitrary levels of detail, and didn't allow for easy manipulation and substitution (e.g. that `x = 2` might mean something different from `x + 3 = 5` is not just added complexity, but makes it hard to describe the relationship between specifications of the same system at different levels of detail). Lamport decided to ditch the older style in favour of one based almost solely on simple mathematics (there were some earlier attempts, but they were still more programming-like than TLA+). He didn't expect that mathematics at the level taught in an introductory, first-semester university course would be so unapproachable to programmers.

082349872349872 1y ago
Wetware programmers may have found the mathematics unapproachable, but what about the LLMs?
jackdaniels4me 1y ago
Lamport didn't design TLA+ for model checking or for practicing developers to use. He did purely for publishing papers where the researchers express their proofs as math (his new TLA+) instead of free form text.
- pron 1y ago
  TLA+ was specifically designed for practitioners (https://lamport.azurewebsites.net/tla/book.html https://lamport.azurewebsites.net/tla/book.html), although he did use earlier incarnations of TLA to analyse his own concurrent and distributed algorithms. His paper explaining TLA [1] says: > We are motivated not by an abstract ideal of elegance, but by the practical problem of reasoning about real algorithms. Rigorous reasoning is the only way to avoid subtle errors in concurrent algorithms, and we want to make reasoning as simple as possible by making the underlying formalism simple. The introduction to the book says: > TLA provides a mathematical foundation for describing systems. To write specifications, we need a complete language built atop that foundation. I ini- tially thought that this language should be some sort of abstract programming language whose semantics would be based on TLA. I didn’t know what kind of programming language constructs would be best, so I decided to start writing specifications directly in TLA. I intended to introduce programming constructs as I needed them. To my surprise, I discovered that I didn’t need them. What I needed was a robust language for writing mathematics. > Although mathematicians have developed the science of writing formulas, they haven’t turned that science into an engineering discipline. ... The specification of a real system can be dozens or even hundreds of pages long. Mathematicians know how to write 20-line formulas, not 20-page formulas. So, I had to introduce notations for writing long formulas. What I took from programming languages were ideas for modularizing large specifications. And the Getting Started portion says: > A system specification consists of a lot of ordinary mathematics glued together with a tiny bit of temporal logic. That’s why most TLA+ constructs are for expressing ordinary mathematics. To write specifications, you have to be familiar with this ordinary math. Unfortunately, the computer science departments in many universities apparently believe that fluency in C++ is more important than a sound education in elementary mathematics. So, some readers may be unfamiliar with the math needed to write specifications. Fortunately, this math is quite simple. If exposure to C++ hasn’t destroyed your ability to think logically, you should have no trouble filling any gaps in your mathematics education. He recognises the tradeoffs of abandoning the programming style, but it is done to make the language simple and practitioner-friendly (and it is a much simpler language than Python, let alone any other specification language, all while preserving maximal expressive power). You can have an opinion on whether this is a good tradeoff or not, but it was done intentionally, and with the purpose of helping practitioners. [1]: https://lamport.azurewebsites.net/pubs/lamport-actions.pdf https://lamport.azurewebsites.net/pubs/lamport-actions.pdf

deterministic 1y ago

Transactional vs. Reactive systems is not a good way to think about it IMHO. A "Reactive system" is basically a "Transactional system" that in addition takes a system state as input and returns a (updated) system state as output: reactive_system : (State * Input) -> (State * Output) Which makes it identical (from a formal point of view) to a "Transactional system".