5

I recently listened to an episode of Software Engineering Radio in which Leslie Lamport was interviewed. One thing he discussed was his specification language, TLA+.

Essentially, he seemed to be arguing that, for programs where correctness is very important, we need to think carefully and specify carefully before writing code, and TLA+ is meant to be a tool to do that. He said a team at Amazon has recently had success using it.

Personally, I write executable tests for my code. I see the tests as a specification, which has the huge benefit of proving whether the code conforms to it.

I assume that Mr. Lamport, being a brilliant and accomplished computer scientist, has long known about this, and still sees a need for his language. But why?

Are formal specification languages and automated tests complementary approaches, or at odds? Do they lend themselves to different kinds of code?

Improve this question
  • 4
    Tests are not a specification nor proof of conformance to a specification, for reasons Killian already brought up in his answer. – Doval May 20 '14 at 12:58
  • 1
    recommended reading: Discuss this ${blog} – gnat May 20 '14 at 13:18
  • I am curious how specifications and executable code have become confused among developers. Lately I have heard several people claim that tests are specifications. The distinction seems to no longer be made in schools or books? – Frank Hileman Jun 17 '14 at 15:31
  • 1
    @FrankHileman I have no formal training, so I can't speak for schools, but I hear devs embracing Agile as opposed to "waterfall" methodology. "Big Design Up Front" is seen as likely to lead to software that doesn't meet actual needs. If there's confusion here, maybe it's equating all non-executable specifications with waterfall design? – Nathan Long Jun 19 '14 at 13:05
  • 1
    @NathanLong: I think you may be right. There may be a negative connotation associated with the word "specification". The best specification is part of the code and verified by a prover... someday it will be standard and built into most compilers. – Frank Hileman Jun 19 '14 at 22:30
4

Your tests can show that the system reacts correctly to those inputs that the tests actually exercise. That is very valuable, but it is nigh-impossible to exercise all inputs that a program might receive.

A judiciously chosen formal proof or specification language document can prove mathematically that your program will respond correctly to all inputs it could possibly receive, even if that is an infinite set. That is certainly better, although whether or not the extra effort is worth the improvement in reliability varies from case to case.

Improve this answer
  • The cost of a proof also varies from language to language; proving that something is correct in an imperative language is incredibly difficult, because most variables could be null and there's side effects all over the place. If the language is dynamically typed on top of that, it's practically hopeless. In a language like Standard ML, where there's no null, no implementation inheritance, mutation is heavily discouraged and the module system allows you to ensure there's only one implementation of an abstraction, the task is substantially easier. – Doval May 20 '14 at 12:53
  • Automated tests can also be invariant. Eg, QuickCheck in Haskell and tools like it let you specify things like, "for any possible list of integers, the reverse function should produce a list with the following properties: contains the same number of elements, first element is now last, all elements still integers... [etc]". So it tests against a large number of randomly chosen inputs and shows you which ones fail. Though admittedly, "a large number of inputs" is not infinite. – Nathan Long May 20 '14 at 12:54
  • @NathanLong Not everything can be tested at runtime. E.g. Can you test that a function doesn't go into an infinite loop? Or that two functions are equivalent? – Doval May 20 '14 at 13:51
  • @Doval Hmmm. No, that's the halting problem. :) But how can you prove that a function doesn't go into an infinite loop without running it, either? Any analysis would involve simulating execution, wouldn't it? "Then if it reached this point and X was 5..." I guess I'm having a hard time envisioning the formal proof without a concrete example. – Nathan Long May 20 '14 at 18:22
  • 1
    @NathanLong Consider a recursive function to calculate the size of a binary tree: when given an empty tree, you return 0; when given a non-empty tree, you return 1 + size(leftChild) + size(rightChild). The base case (empty tree) terminates, since all it does is return a constant value. The non-base case only does addition (we know this terminates) and recursive calls. The recursive calls always operate on an immediate child; therefore, the recursion will always reach the base case, which terminates. These are the only two possibilities. Q.E.D. – Doval May 20 '14 at 18:38
3

Personally, I write executable tests for my code. I see the tests as a specification, which has the huge benefit of proving whether the code conforms to it.

This is not a proof. If you think of the semantics of your program (or embedded computer system), it has an infinity (or a large number) of states. Be aware of the halting problem, related undecidable problems, intractability, The P vs NP problem, and the Curry-Howard correspondence. Remember what D.Knuth told of proving software and testing it. Be also aware of declarative programming paradigms and even, in the long term -decades at least-, serious AGI research (like this), related to autonomous robots or vehicles. See also this.

Consider for example a cheap Arduino Uno system (very often used in hobby embedded devices). It has 2Kbytes of RAM. So 2048*8, that is 16384 bits. So it has 216384 states (a very huge number). Add to that the states modeling your abstracted view of the (physical) environment dealt with your Arduino. Assume you have only 10 of them for your device. Then your entire system has 2(16384+10) states and could be viewed as a finite state automaton around them. How much states did you tested with your executable tests? Only a small fraction of them!

A proof is "mathematical" (for some view of mathematics, and some definition of proofs).

See also the difference between DO-178C and its predecessor DO-178B.

Read also the first chapter of my Bismon draft report. It discusses, and give more details than I could give here, your question.

Executable tests and formal proofs are complementary, not competitors. You need both for safety-critical embedded digital systems.

Formal proofs tend to move bugs' opportunity even upper: less bugs in code, but perhaps more bugs in the formalized specifications. In safety-critical systems, both could kill.

My opinion is that, in addition, safety-critical software should be free software (at least to be reviewable by other citizens having software development expertise). But this is a dream. I expect thousands of deaths because most of such vital software are, today, still proprietary, and developed with social, regulatory, and business constraints that are not questioned enough.

Improve this answer
2

Mr. Lamport, ... still sees a need for his language. But why?

With a formal specification language, you can run a verifier - that proves the design/algorithm mathematically. This is not the same as a set of unit/integration/bdd tests.

Are formal specification languages and automated tests complementary approaches, or at odds?

These are complementary, certainly. Nothing stops you from using both, if needed.

Improve this answer
  • "you can run a verifier - that proves the design/algorithm mathematically" - so it proves it in a way that does not rely on trying lots of examples, as does invariant testing? – Nathan Long May 20 '14 at 12:58
  • 1
    @NathanLong - as I understand it (and I don't claim deep understanding) - but it is a verifier that looks at the consistency of the formal specification and any "holes" - anything that isn't proven. – Oded May 20 '14 at 13:09

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.