Formal specs as sets of behaviors
surfingcomplexity.blog
Formal specs as sets of behaviors
1–10 of 19 posts
Re: Formal specs as sets of behaviors
#2There’s definitely some good patterns in here. Needs worked examples
Re: Formal specs as sets of behaviors
#3I was hoping for a TLA+ example, but it never got there.
Re: Formal specs as sets of behaviors
#4As 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/EWD101...
Re: Formal specs as sets of behaviors
#5> 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.
Re: Formal specs as sets of behaviors
#6As 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 thi…
>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?
Re: Formal specs as sets of behaviors
#7I was hoping for a TLA+ example, but it never got there.
Hillel Wayne's "Practical TLA+" book and the TLA+ examples repository (https://github.com/tlaplus/Examples) both contain excellent worked examples ranging from simple algorithms to complex distributed systems.
Re: Formal specs as sets of behaviors
#8As 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 thi…
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).
Re: Formal specs as sets of behaviors
#9As 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 thi…
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 a…
P.S.
A model checker doesn't imply anything about the kind of the formal specification used. It is a program that checks whether all assignments of free variables in a formula are satisfying assignments, or "models" for the formula (a model is a satisfying assignement of free variables in a formula, i.e. assignments that make the formula true).
It is distinct from an automated proof finder in that it doesn't (necessarily) find a deductive proof in the relevant logic that the forumla is always true, but rather operates in the semantic universe of the logic.
For example, the proposition `A ⇒ A` is true for any A in a simple boolean logic. We can determine that either via a deductive proof, which consists of a sequence of application of the deductive rules of the logic, or by examining the relevant truth table; the latter method would be a form of model checking.
Neither the use of deductive proofs or of model checking implies something about the nature of the logic. They are just two different ways of determining the truth of a proposition.
Re: Formal specs as sets of behaviors
#10Earlier quoted context omitted.
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 a…
P.S. A model checker doesn't imply anything about the kind of the formal specification used. It is a program that checks whether all assignments of free variables in a formula are satisfying assignments, or "models" for the formula (a model is a satisfying assignement of free variables in a formula, i.e. assignments that make the formula true). It is distinct from an automated proof finder in that it doesn't (necessa…
> A model checker doesn't imply anything about the kind of the formal specification used.
That is true; I was just contrasting the way TFA explained specifications as being definitions of groups of acceptable execution traces (perhaps checked using a model checker) with Dijkstra’s approach of characterizing the acceptable behavior without simulating any executions.
Both are of course valid approaches to demonstrate the correctness of a specification.