4 ms·

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a ver

Heh, eh, well, ah, ... (and other strange noises). Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) Anyway, if you want a better specification language based on GCL, check out Jayadev Misra's UNITY (A Discipline of Multiprogramming, Springer-Verlag, 2001.) or Mohamed Gouda's Abstract Protocols (Elements of network protocol design, Whiley 2008.)

hwayne 3y ago
there are too many specification languages
- mcguire 3y ago
  Ooohhhh, a specification language for specification languages. The grammar that ties together graphical things like Petri Nets and TLA+ is going to be fantastic!
  - hwayne 3y ago
    Unrelated but the coolest thing I discovered while researching this piece was that Petri Net reachability is decidable but Ackermann-complete. ACK-COMPLETE is a thing. That's wild.
    - sterlind 3y ago
      what does that mean exactly? I skimmed the paper you linked briefly, but couldn't quite tell. Does it mean that deciding reachability of an N-state petri net takes Ack(N) steps in the worst case? Or that you can can construct a Petri net which has a node reachable after Ack(N) steps? Those are different I think since you can compute Ack(N) in fewer than Ack(N) steps. I also wonder if you can more efficiently rule out polynomial-time reachability of a Petri net node, even if it is eventually reachable.
      - hwayne 3y ago
        The former, though it grows a little slower than Ack(N). If I read the paper write, they showed that an 18-state Petri Net has a worst case reachability problem on the order of Ack(3), and then every six states you add, n goes up by one. So a 24 state Petri net can take Ack(4) steps to decide, for a 30 state Petri net Ack(5), etc. This is just the decision problem, not the length of the path. (The paper is actually works on *Vector Addition Systems*, but VASes are isomorphic to Petri nets.) Note these are loose boundaries: adding at most six states will definitely bump the hardness by at least 1, but it might grow faster than that. At the end of the paper they note some people have gotten more precise boundaries, that 10-states is "Tower-hard" (Ack(3)), and every 2 states bumps it by 1. So worst case for a 12-state net is on the order of Ack(4), etc.
User23 3y ago
> Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined by Dijkstra and Scholten (among others, but they're the ones best known to me). So in that sense the ur-language for program specification is something we might call "mathematical logic." And predicate transformer semantics, when you get right down to it, is leaning on Leibniz's principle about as hard as biology leans on H-bonds. As you say, GCL is just a simple language that has a well defined predicate transformer semantic and an interesting approach to nondeterminism that is suitable for the kind of research Dijkstra was doing. One could theoretically define predicate transformer semantics for any language, although it would be a prohibitively difficult challenge for most if not all languages in common use today. Whether that's a problem with predicate transformer semantics or the languages we have is a matter of opinion I suppose. Also predicate transformer semantics were extended to support concurrency by Lamport[1]. I'm still hoping for the day when assertional arguments fully banish behavioral ones, but it looks like it's still a long way off. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf
- mcguire 3y ago
  For some reason, I ended up calling those "axiomatic semantics"; predicate transformer semantics is a much better name. One of the weaknesses of PTS for common languages is that statements and expressions have very complicated semantics, compared to the relatively simple semantics of GCL and other simple treatments. One of the nice things about Frama-C (and I think the GNAT SPARK tools) is that, when you are using the WP (Weakest Precondition) module to prove properties of C code, it can automatically generate assertions that describe overflow/underflow, which then forces you to put the appropriate preconditions on function parameters. :-) By the way, have you run across K. Rustan M. Leino's recent book, Program Proofs, and the Dafny language. It's the most recent and so far, best book I've seen on the style and technology.
  - 3y ago

hwayne 3y ago

there are too many specification languages

mcguire 3y ago
Ooohhhh, a specification language for specification languages. The grammar that ties together graphical things like Petri Nets and TLA+ is going to be fantastic!
- hwayne 3y ago
  Unrelated but the coolest thing I discovered while researching this piece was that Petri Net reachability is decidable but Ackermann-complete. ACK-COMPLETE is a thing. That's wild.
  - sterlind 3y ago
    what does that mean exactly? I skimmed the paper you linked briefly, but couldn't quite tell. Does it mean that deciding reachability of an N-state petri net takes Ack(N) steps in the worst case? Or that you can can construct a Petri net which has a node reachable after Ack(N) steps? Those are different I think since you can compute Ack(N) in fewer than Ack(N) steps. I also wonder if you can more efficiently rule out polynomial-time reachability of a Petri net node, even if it is eventually reachable.
    - hwayne 3y ago
      The former, though it grows a little slower than Ack(N). If I read the paper write, they showed that an 18-state Petri Net has a worst case reachability problem on the order of Ack(3), and then every six states you add, n goes up by one. So a 24 state Petri net can take Ack(4) steps to decide, for a 30 state Petri net Ack(5), etc. This is just the decision problem, not the length of the path. (The paper is actually works on *Vector Addition Systems*, but VASes are isomorphic to Petri nets.) Note these are loose boundaries: adding at most six states will definitely bump the hardness by at least 1, but it might grow faster than that. At the end of the paper they note some people have gotten more precise boundaries, that 10-states is "Tower-hard" (Ack(3)), and every 2 states bumps it by 1. So worst case for a 12-state net is on the order of Ack(4), etc.

User23 3y ago

> Dijkstra's Guarded Command Language is a specification language, sort of, but it's better looked at as a very simple programming language for use with Floyd/Hoare/Dijkstra's axiomatic semantics. (Which didn't get mentioned at all. Sniff.) This struck me too. There is an ur-language there, but it's not GCL rather it's Hoare triples and subsequently predicate transformer semantics and Boolean structures, as defined by Dijkstra and Scholten (among others, but they're the ones best known to me). So in that sense the ur-language for program specification is something we might call "mathematical logic." And predicate transformer semantics, when you get right down to it, is leaning on Leibniz's principle about as hard as biology leans on H-bonds. As you say, GCL is just a simple language that has a well defined predicate transformer semantic and an interesting approach to nondeterminism that is suitable for the kind of research Dijkstra was doing. One could theoretically define predicate transformer semantics for any language, although it would be a prohibitively difficult challenge for most if not all languages in common use today. Whether that's a problem with predicate transformer semantics or the languages we have is a matter of opinion I suppose. Also predicate transformer semantics were extended to support concurrency by Lamport[1]. I'm still hoping for the day when assertional arguments fully banish behavioral ones, but it looks like it's still a long way off. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf

mcguire 3y ago
For some reason, I ended up calling those "axiomatic semantics"; predicate transformer semantics is a much better name. One of the weaknesses of PTS for common languages is that statements and expressions have very complicated semantics, compared to the relatively simple semantics of GCL and other simple treatments. One of the nice things about Frama-C (and I think the GNAT SPARK tools) is that, when you are using the WP (Weakest Precondition) module to prove properties of C code, it can automatically generate assertions that describe overflow/underflow, which then forces you to put the appropriate preconditions on function parameters. :-) By the way, have you run across K. Rustan M. Leino's recent book, Program Proofs, and the Dafny language. It's the most recent and so far, best book I've seen on the style and technology.
- 3y ago