Decision Tables
hillelwayne.com
hillelwayne.com
[1]: E.g. trace-checking: https://arxiv.org/pdf/1111.2825.pdf
What about modern dependently-typed meta languages like Idris and program synthesizers like Nadia Polikarpova's work on Synquid?
Type-Driven Program Synthesis, by Nadia Polikarpova (StrangeLoop 2018) [video] https://www.youtube.com/watch?v=HnOix9TFy1A
MIT Comcom: Synquid program synthesizer, and more command-line tools for the web
http://comcom.csail.mit.edu/comcom/
Idris Software Foundations https://github.com/idris-hackers/software-foundations
The biggest programs ever written and verified with deductive proofs -- be it dependently typed languages or any verification based on deduction, correspond at most to ~10,000 LOC of C, taken years of work by academic experts, and had to be significantly simplified to make proofs easier (i.e., they had to use only the simplest data structures, etc.). In contrast, business applications are 2-3 orders of magnitude bigger.
[1]: And when I say "we don't know" I mean that it is possible that some time in the next 2-5 decades we may be able to do something, but it's also possible that there are fundamental complexity limitations that mean that this particular path will never lead to something similar to what we may imagine it could.
Take the IRC RFC, for instance. A lot of it is amenable to code generation, but machine-parsing the spec is so hard (I know.. I tried, many moons ago). I feel like a big chunk of that spec could be written in such way that a big part of an IRC client or server could be generated. For other parts, a generator could at least create boilerplate to be filled by a human and maybe some automatic tests.
I don't think it's the bare minimum, as an informal specification is far better than none at all, but I agree that a formal specification is better -- at least in the more complicated cases -- as it forces precision and also allows the use of tools that could check it in various ways.
Sure, but I'm talking about this article about decision tables. We don't have to spec the entire program in an executable way. We can just take part of the logic, encode it as a decision table, and declare that this is the spec. Then we read it in to the program and execute it. Nothing intractable about it! (Or if there is, then no self-consistent spec is possible in the first place.)
But I don't agree that encoding the decision table is boring and easy -- if the business logic is complex enough to require a spec. The good news is that now the table itself is all we need -- no self-written code, and no separate spec.
My point was that it doesn't matter how good his system is, as long as he doesn't separate declaration from implementation, it will be of almost no use. Nobody will be able to run his Mercury program in 100 years from now. Then again, it's not possible to run my Higher Order Logic with Henkin models and Categorial Grammar out of the box either.
So I'm still not sure who had the better argument. Maybe if researchers could agree on a common programming language, we could indeed dispense with descriptive formalisms?
Lacking code, however, usually leads to important oversights in the specifications. Internet routers had to have a "compatible with Cisco" option because Cisco engineers read a specification, wrote an implementation, had no reference code to test against, and ended up with a widely deployed broken protocol incompatible with the correct version.
Code is critical for specifications because it doesn't suffer the flaws of human interpretation and assumptions. If it does disagree with human interpretations of the specification then it quickly becomes obvious and either the code or specification can be fixed in a revision.
Code is a formal specification at a very particular level. But you can have formal specifications of any level you like that is just as precise and mechanical as code (and usually much clearer).
match n mod 3 = 0, n mod 5 = 0 with
| true, true -> "FizzBuzz"
| true, false -> "Fizz"
| false, true -> "Buzz"
| false, false -> string_of_int n
This a "cleaner" version that takes advantage of wildcards (which appear in the article, but not in the FizzBuzz): match n mod 3, n mod 5 with
| 0, 0 -> "FizzBuzz"
| 0, _ -> "Fizz"
| _, 0 -> "Buzz"
| _, _ -> string_of_int n
Note that the article states, "two rows can’t overlap in what inputs they cover," but in case analyses expressions of PLs with pattern matching, two rows can share a non-empty set of common matches and the higher row will take precedence.In this case, the most optimal representation of the data is the code.
Well, I could write another tool to analyse it, eg extract some statistics; I could write another tool to generate it, eg based on data.
(Maybe I'm being unfair here. I write mostly Elixir, and it's really easy in Elixir—one or two lines—to extract the AST of the body of a function defined in a given file and then work with it. It's just as easy to hold data canonically in its AST representation, and then both analyze it, and generate code from it, at runtime.)
for i in 0...100 {
switch (i % 3, i % 5) {
case (0, 0): print("FizzBuzz")
case (0, _): print("Fizz")
case (_, 0): print("Buzz")
case (_, _): print("\(i)")
}
} def fizzbuzz(x) when is_integer(x) do
case {rem(x, 3), rem(x, 5)} do
{0, 0} -> "FizzBuzz"
{0, _} -> "Fizz"
{_, 0} -> "Buzz"
{_, _} -> Integer.to_string(x)
end
end(I apologise for this Python abomination):
print([{ (True, True): 'Fizzbuzz', (True, False): 'Fizz', (False, True): 'Buzz', (False, False): i }[i % 3 == 0, i % 5 == 0] for i in range(1, 101)])It's almost always easier to read if you don't indent it, though HN should probably fix their style sheets so it doesn't matter.
If I'm quoting something (another reason people often indent their comments) I will normally wrap the whole thing in * so that it is italicised.
I don't know a good way to make code stand out, maybe someone else has an idea.
Personally I prefer putting a greater than sign in front of each paragraph I am quoting / quoting from.
It’s what we do in e-mail and on most imageboards and in markdown. It’s easy to read and easy to understand that it’s a quote.
Sure, we could write a loop with an if-else-if-else block inside to implement a state machine, but once we understand the formalism properly it might be better to use a generic piece of code to run the state machine, and a data structure mapping (state, input) pairs to actions/outputs.
Similarly, we could write a big if-else-if-else to implement our business logic, but once we recognise that we have a decision table, we are better using a generic piece of code to implement the decision table idea, and storing our logic in a table.
In both cases we are separating logic from data.
Also relevant to decision tables, since they're far more efficient for some situations, is decision trees. Many people are familiar with decision trees as a machine learning method, or as a method for analysing a decision (utility, probabilities, etc.), but they can also be used to express the same logic as a decision table as in this article. Again, a generic piece of code can execute the decision tree, and the tree itself can be stored as data.
understood state machines.
Of course decision tables and (finite) state machines are essentially the same: each FSM induces a decision table (indexed by current state and current action) and vice versa. #lang 2d racket
(require 2d/match)
(define (subtype? a b)
#2dmatch
╔══════════╦══════════╦═══════╦══════════╗
║ a b ║ 'Integer ║ 'Real ║ 'Complex ║
╠══════════╬══════════╩═══════╩══════════╣
║ 'Integer ║ #t ║
╠══════════╬══════════╗ ║
║ 'Real ║ ║ ║
╠══════════╣ ╚═══════╗ ║
║ 'Complex ║ #f ║ ║
╚══════════╩══════════════════╩══════════╝)
https://docs.racket-lang.org/2d/index.html f(t, t, t) -> 1;
f(t, t, f) -> 3;
f(t, f, t) -> 7;
f(t, f, f) -> "cucumber";
f(f, _, _) -> null.
Pretty close to the table, no?The other example:
fizzbuzz(N) ->
case {N rem 3, N rem 5} of
{0, 0} -> "FizzBuzz";
{0, _} -> "Fizz";
{_, 0} -> "Buzz";
{_, _} -> N
end.
Here I used a case statement, but it also matches the shape pretty well.That's valid code, not pseudocode, you can compile it in a module an run it.
Notice how multiple function clauses separated by ; allow much nicer code patches. If a function wasn't working well, instead of adding an if statement inside, you can add another function clause instead.
"a cross between decision tables and data flow graphs"
I had a textbook that had a whole chapter about this, I will find the title and edit this post.
EDIT: A Practitioner's Guide to Software Test Design, Lee Copeland, Artech House (January 2004), ISBN-13: 978-1580537919.
Truth tables can eliminate a lot of ambiguity compared to a wall of text or dozens of bullet-point requirements.
The best part? It was loaded into a running service by parsing a complex Excel spreadsheet which lead to so much fun with debugging.
You could probably expand this method to other forms.
[1]: https://www.wikiwand.com/en/Truth_table [2]: https://www.wikiwand.com/en/Karnaugh_map