2

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. Laport, 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
  • 2
    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
  • @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
2

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
0

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
  • @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.