6 ms·

Machine Readable Specifications at Scale

37 points by fanf2 5y ago

golf_mike 5y ago
So what would such a language look like?
- eternalban 5y ago
  A 'table' scheme for syntactic forms which would be compiled to an FSM (equiv to a regular) language for processing. Assuming each row has a tuple value, any document definition language (such as JSON) would do as the front-end that spits out the RL. https://en.wikipedia.org/wiki/Regular_language https://en.wikipedia.org/wiki/Regular_language
  - airbreather 5y ago
    I am a functional safety engineer for industrial plant and equipment and this exactly what I do for designing the sequencing and safety systems for large fired equipment. Either single FSM or a hierarchy of them when there is multiple burners. I wrote myself a package using PyQt that sort of looks like a special spreadsheet that allows the combustion engineers to specify and also simulate the logic on a scan by scan basis. The supporting logic "engine" is actually so simple as to be effectively 4 bitwise ops on bit packed words, per state (I use Mealy machines so the outputs are coupled directly and synchronously to states). Bonus is first up alarms and whats holding you out from next state all come for free in the logic used and you can derive a bunch of test cases automatically. The sim/spec tool could export code ready to import to the controller, but we haven't had the economies of scale to support the required generalised tool testing this would require, but it does generate a bunch of hex codes that are the "configuration" that controls the functionality, interpreted by the 'engine' A bunch of other bonuses, it allows you collect notes in a rich text doc behind every transition or condition cell and it can export these to make an easier to read human readable spec, it has an OPC server so you can couple it up to a HMI and do some basioc training or simulation demonstration, or you can bolt it onto an existing machine and see how well it "shadows" it if you are doign a retrofit or brownfields job. The improved quality of outcomes and traceability etc (all the good engineering things desireable) yielded by an executable specification has increased by at least an order of magnitude by having a tool of this nature. Previously most systems like this were effectively done by specifying with a "crappy narrative". This usually entailed, at best, a collection of vague thoughts about some things that were wanted, and some things that weren't, often some in conflict, and a not mentioning a bunch of negelected things. You then rolled the dice on the programmer and hoped they knew enough to ask the 3000 needed questions to somehow come up with adequately coded functionality. New tool is way, way better. A final note, a joke I am sure most of you know, about why English is a poor specifying language and the sort of thing that drove me to take this path (with English it's all about assumed context) A wife asks her husband, a software engineer, "Could you please go shopping for me and buy one carton of milk, and if they have eggs, get 6!" A short time later the husband comes back with 6 cartons of milk. The wife asks him, "Why the hell did you buy 6 cartons of milk?" He replied, "They had eggs."
- choeger 5y ago
  More interestingly: What would it mean? What is actually specified? For instance, when I specify a messaging protocol I could use a FSM but would this implicitly assume that there is some form of "connection" between client and server that consists of a state in each of them. So whenever I specify something, I need to start with a declaration of the entities and the list of possible events (and these events would carry data). This way, the spec has an unintended effect on the implementation. Let's assume that I have some universal way to represent this data in all target languages (complicated but doable). If I then want to compile this FSM spec into test cases, I must offer some interface that mirrors the entities and events, essentially forcing me to explicitly program a FSM. This is suboptimal because my implementation might not actually need this level of abstraction. A simple embedded C program might be described as a FSM but it could be implemented as a sequence of instructions. Of course, we could also switch to integration testing, passing messages over sockets, etc. but then we would have to program the scaffolding around our mock client/server component and to benefit from the automatic test case generation we would have to either parse and interpret these automatic test cases or program our mock in a form that is defined by the specification output. What I am trying to say is that there probably won't be a universal spec language. Instead, it should fit into the implementation eco system.
mch82 5y ago
> This is incredibly valuable because a good testsuite lets you check your specification. Could the test suite actually serve as the specification?
- chriswarbo 5y ago
  Tests are specifications, but they can only encode "there exists" statements. For example, consider a test like this: def canUpdateUsername(): u = User("u1", "user@example.com") n = "u2" assert u.setUsername(n).getUsername() == n As a specification, this states that there exists a user 'u' and a username 'n', such that u.setUsername(n).getUsername() equals n. We prove that statement by providing explicit examples of 'u' (the value User("u1", "user@example.com")) and 'n' (the value "u2"), and the computer checks the proof by executing the code. That execution is equivalent to substituting-in/inlining definitions, and rewriting primitives like 'if (True): x', until we get the value 'True'. QED. Usually what we actually want is a "for all" statement. Sometimes tests can achieve this by being exhaustive, e.g. checking every boolean, or all 256 bytes. More generally, a "for all" statement is a function, e.g. def canUpdateUsernames(u: User, n: str): assert u.setUsername(n).getUsername() == n This is a better specification, since we're asserting the relationship between 'setUsername' and 'getUsername' for any/every User and string. Unfortunately, we can't prove this by substituting-in/inlining definitions, since we don't have definitions for 'u' and 'n'. One way to prove it is to use a more general approach, e.g. using equational rewriting, induction, etc. That's the approach taken by (interactive) theorem provers, but it can be a lot of work. Systems I've used for this include https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what... https://coq.inria.fr https://coq.inria.fr https://www.idris-lang.org https://www.idris-lang.org and https://isabelle.in.tum.de https://isabelle.in.tum.de An easier alternative is to try disproving the statement, by executing it on thousands of examples and seeing if any fail. That gives us less confidence than a full proof, but can still be better than traditional "there exists" tests. This is called property checking or property-based testing. Systems I've used for this include https://hypothesis.works https://hypothesis.works https://hackage.haskell.org/package/QuickCheck https://hackage.haskell.org/package/QuickCheck https://scalacheck.org https://scalacheck.org and https://jsverify.github.io https://jsverify.github.io
pfdietz 5y ago
What I want to see is a specification language that can be compiled to natural language. This should be easier than trying to parse a natural language specification into something more machine readable. Standards documents are already quite often very stereotyped, so "compiling" to them seems like a good step. There would be a backup to insert unstructured (if perhaps parameterized) text, but it would have to be made somewhat awkward to discourage its use.
- xg15 5y ago
  I think "natural language" is underspecified. E.g. it probably wouldn't be that hard to write some kind of templating engine that takes an XSL schema and outputs something resembling plain English. Except, the output would likely read like the most horrible legalese you can imagine. Then you have some like the algorithmic definitions that proliferate most of the web platform/HTML5 specs. Those are all "cookbook style" lists of steps written in plain English - and it's easy to understand what an individual step does. However, understanding what the whole algorithm does - or even more, why it does what the spec says - is just as hard as it would be with code or pseudocode.
  - pfdietz 5y ago
    The reason I want this is not to make the standards easier for people to understand. Sure, the standards will be in legalese. But they are already in legalese. The goal is to make the standards more comprehensible to machines as well, without further degrading their (already problematic) comprehensibility to humans. Kill two birds with one stone.
    - xg15 5y ago
      Have a look at the WHATWG specs then - this might be a lot like what you want. E.g. Fetch [1]. Effectively, most of the spec could be written in pseudocode, except they expanded each pseudocode line into a complete sentence and annotated the whole thing with markers, links and commentary. The result is the afromentioned "cookbook style". I'm not sure if this is actually easier to read than pseudocode though. [1] https://fetch.spec.whatwg.org/#fetching https://fetch.spec.whatwg.org/#fetching
vivegi 5y ago
TLA+ from MSFT Research is a formal specification language. See: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html Leslie Lamport, the author, mentions some examples of industrial use of TLA+ at MSFT, Intel, Amazon and a few other orgs. https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus
continuational 5y ago
We have an internal JSON format for specifying the firewall configurations of all our servers. Essentially just "this group of servers can access this group of servers on these ports". Together with an idempotent "make it so" script, it has been a lifesaver.
Charles33 5y ago
[dead]

37 points by fanf2 5y ago

golf_mike 5y ago

So what would such a language look like?

eternalban 5y ago
A 'table' scheme for syntactic forms which would be compiled to an FSM (equiv to a regular) language for processing. Assuming each row has a tuple value, any document definition language (such as JSON) would do as the front-end that spits out the RL. https://en.wikipedia.org/wiki/Regular_language https://en.wikipedia.org/wiki/Regular_language
- airbreather 5y ago
  I am a functional safety engineer for industrial plant and equipment and this exactly what I do for designing the sequencing and safety systems for large fired equipment. Either single FSM or a hierarchy of them when there is multiple burners. I wrote myself a package using PyQt that sort of looks like a special spreadsheet that allows the combustion engineers to specify and also simulate the logic on a scan by scan basis. The supporting logic "engine" is actually so simple as to be effectively 4 bitwise ops on bit packed words, per state (I use Mealy machines so the outputs are coupled directly and synchronously to states). Bonus is first up alarms and whats holding you out from next state all come for free in the logic used and you can derive a bunch of test cases automatically. The sim/spec tool could export code ready to import to the controller, but we haven't had the economies of scale to support the required generalised tool testing this would require, but it does generate a bunch of hex codes that are the "configuration" that controls the functionality, interpreted by the 'engine' A bunch of other bonuses, it allows you collect notes in a rich text doc behind every transition or condition cell and it can export these to make an easier to read human readable spec, it has an OPC server so you can couple it up to a HMI and do some basioc training or simulation demonstration, or you can bolt it onto an existing machine and see how well it "shadows" it if you are doign a retrofit or brownfields job. The improved quality of outcomes and traceability etc (all the good engineering things desireable) yielded by an executable specification has increased by at least an order of magnitude by having a tool of this nature. Previously most systems like this were effectively done by specifying with a "crappy narrative". This usually entailed, at best, a collection of vague thoughts about some things that were wanted, and some things that weren't, often some in conflict, and a not mentioning a bunch of negelected things. You then rolled the dice on the programmer and hoped they knew enough to ask the 3000 needed questions to somehow come up with adequately coded functionality. New tool is way, way better. A final note, a joke I am sure most of you know, about why English is a poor specifying language and the sort of thing that drove me to take this path (with English it's all about assumed context) A wife asks her husband, a software engineer, "Could you please go shopping for me and buy one carton of milk, and if they have eggs, get 6!" A short time later the husband comes back with 6 cartons of milk. The wife asks him, "Why the hell did you buy 6 cartons of milk?" He replied, "They had eggs."
choeger 5y ago
More interestingly: What would it mean? What is actually specified? For instance, when I specify a messaging protocol I could use a FSM but would this implicitly assume that there is some form of "connection" between client and server that consists of a state in each of them. So whenever I specify something, I need to start with a declaration of the entities and the list of possible events (and these events would carry data). This way, the spec has an unintended effect on the implementation. Let's assume that I have some universal way to represent this data in all target languages (complicated but doable). If I then want to compile this FSM spec into test cases, I must offer some interface that mirrors the entities and events, essentially forcing me to explicitly program a FSM. This is suboptimal because my implementation might not actually need this level of abstraction. A simple embedded C program might be described as a FSM but it could be implemented as a sequence of instructions. Of course, we could also switch to integration testing, passing messages over sockets, etc. but then we would have to program the scaffolding around our mock client/server component and to benefit from the automatic test case generation we would have to either parse and interpret these automatic test cases or program our mock in a form that is defined by the specification output. What I am trying to say is that there probably won't be a universal spec language. Instead, it should fit into the implementation eco system.

mch82 5y ago

> This is incredibly valuable because a good testsuite lets you check your specification. Could the test suite actually serve as the specification?

chriswarbo 5y ago
Tests are specifications, but they can only encode "there exists" statements. For example, consider a test like this: def canUpdateUsername(): u = User("u1", "user@example.com") n = "u2" assert u.setUsername(n).getUsername() == n As a specification, this states that there exists a user 'u' and a username 'n', such that u.setUsername(n).getUsername() equals n. We prove that statement by providing explicit examples of 'u' (the value User("u1", "user@example.com")) and 'n' (the value "u2"), and the computer checks the proof by executing the code. That execution is equivalent to substituting-in/inlining definitions, and rewriting primitives like 'if (True): x', until we get the value 'True'. QED. Usually what we actually want is a "for all" statement. Sometimes tests can achieve this by being exhaustive, e.g. checking every boolean, or all 256 bytes. More generally, a "for all" statement is a function, e.g. def canUpdateUsernames(u: User, n: str): assert u.setUsername(n).getUsername() == n This is a better specification, since we're asserting the relationship between 'setUsername' and 'getUsername' for any/every User and string. Unfortunately, we can't prove this by substituting-in/inlining definitions, since we don't have definitions for 'u' and 'n'. One way to prove it is to use a more general approach, e.g. using equational rewriting, induction, etc. That's the approach taken by (interactive) theorem provers, but it can be a lot of work. Systems I've used for this include https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what... https://coq.inria.fr https://coq.inria.fr https://www.idris-lang.org https://www.idris-lang.org and https://isabelle.in.tum.de https://isabelle.in.tum.de An easier alternative is to try disproving the statement, by executing it on thousands of examples and seeing if any fail. That gives us less confidence than a full proof, but can still be better than traditional "there exists" tests. This is called property checking or property-based testing. Systems I've used for this include https://hypothesis.works https://hypothesis.works https://hackage.haskell.org/package/QuickCheck https://hackage.haskell.org/package/QuickCheck https://scalacheck.org https://scalacheck.org and https://jsverify.github.io https://jsverify.github.io

pfdietz 5y ago

What I want to see is a specification language that can be compiled to natural language. This should be easier than trying to parse a natural language specification into something more machine readable. Standards documents are already quite often very stereotyped, so "compiling" to them seems like a good step. There would be a backup to insert unstructured (if perhaps parameterized) text, but it would have to be made somewhat awkward to discourage its use.

xg15 5y ago
I think "natural language" is underspecified. E.g. it probably wouldn't be that hard to write some kind of templating engine that takes an XSL schema and outputs something resembling plain English. Except, the output would likely read like the most horrible legalese you can imagine. Then you have some like the algorithmic definitions that proliferate most of the web platform/HTML5 specs. Those are all "cookbook style" lists of steps written in plain English - and it's easy to understand what an individual step does. However, understanding what the whole algorithm does - or even more, why it does what the spec says - is just as hard as it would be with code or pseudocode.
- pfdietz 5y ago
  The reason I want this is not to make the standards easier for people to understand. Sure, the standards will be in legalese. But they are already in legalese. The goal is to make the standards more comprehensible to machines as well, without further degrading their (already problematic) comprehensibility to humans. Kill two birds with one stone.
  - xg15 5y ago
    Have a look at the WHATWG specs then - this might be a lot like what you want. E.g. Fetch [1]. Effectively, most of the spec could be written in pseudocode, except they expanded each pseudocode line into a complete sentence and annotated the whole thing with markers, links and commentary. The result is the afromentioned "cookbook style". I'm not sure if this is actually easier to read than pseudocode though. [1] https://fetch.spec.whatwg.org/#fetching https://fetch.spec.whatwg.org/#fetching

vivegi 5y ago

TLA+ from MSFT Research is a formal specification language. See: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html Leslie Lamport, the author, mentions some examples of industrial use of TLA+ at MSFT, Intel, Amazon and a few other orgs. https://github.com/tlaplus/tlaplus https://github.com/tlaplus/tlaplus

continuational 5y ago

We have an internal JSON format for specifying the firewall configurations of all our servers. Essentially just "this group of servers can access this group of servers on these ports". Together with an idempotent "make it so" script, it has been a lifesaver.

Charles33 5y ago

[dead]