2 ms·

> Tests are specifications No, they're not. Unless you're OK with the system working for only exactly the test cases you specify (which, btw, is trivially imp

> Tests are specifications No, they're not. Unless you're OK with the system working for only exactly the test cases you specify (which, btw, is trivially implementable as a look-up table of the test cases!), tests do not specify a system. EDIT: Importantly, tests have no means of distinguishing for a missing test case whether that case's behavior should be inferred or is actually unspecified. See http://en.wikipedia.org/wiki/Z_notation http://en.wikipedia.org/wiki/Z_notation for an example of an actual serious specification language.

farginay 13y ago
I think it is fairer to say that tests can specify a system but not to the extent that you personally want to.
- colanderman 13y ago
  I don't know; I'd be wary of working with any architect who handed me a list of test cases as a specification. What if he/she left out important edge cases, which I extrapolate incorrectly? How am I to infer that the absence of a test case means "not specified" vs. "specified to be the extrapolation of other test cases"? That's kind of like saying that a coder who can only write pseudocode can code a system, but not to the extent that I personally want him/her to.
  - davidw 13y ago
    I'd be wary of comparing programming to architecture.
  - farginay 13y ago
    Be wary of an architect who hands you anything and tells you to implement it. Real architects talk to you and sit down and write code with you.
thatthatis 13y ago
There's nothing that says any non trivial specification in any language is either complete or correct. Tests _can be_ used as a _kind of_ specification.
- timtadh 13y ago
  > nothing that says any non trivial specification in any language is either complete or correct. Absolutely correct. In fact the larger the specification the more likely that the specification has a bug. > Tests _can be_ used as a _kind of_ specification. Also true. But, frequently in program verification (proving a program does what it is specified to do) specifications are not tests. Why are specification not written as tests? It comes down to the program verification technique which is used. There are several categories: - Testing. "Optimistically Inaccurate" It can't find all problems but all problems it finds are real problems (assuming of course the test is correct). The downside is you may give an OK to a bad program, the upside is when you find a problem it is a real problem. - Dataflow Analysis. "Pessimistically Inaccurate" It can prove fairly general properties about a program. However, it cannot prove all properties and may not be able to prove a property which is true. For example say you where proving a program did not have a SQL injection. Dataflow analysis would OK only programs it could prove the absence of a SQL injections (as per the specification you give it! (there may be a SQL injection your spec doesn't cover)). However, there may be programs which are free of SQL injections but Dataflow Analysis is unable to prove it. - Model Checking. "Pessimistically Inaccurate, Simplified Properties" In model checking you move the program by mapping it into a new domain such as a finite state automaton. You do the mapping in such a way that properties proved about the model must hold in the actual program. Unfortunately, you can only check simplified properties and there is still some pessimistic inaccuracy (although it is reduced from dataflow analysis since the domain is easier to prove properties on). - Syntax Analysis. "Simplified Properties" Eg. Grammar Checking. You can only prove properties that can be found by a parser. You can write checks which have false positives. Eg. the check may fail but the program is fine. Type Checking is another method way as is Theorem Proving. I am sure there are even more methods beyond the ones I listed here. The point is except in the case of testing, the specifications are not given as tests. Each verification technique requires its own formal specification language. However, there are some systems where you can specify a program in a general language which can then be compiled to the verification system you actually use.
tmoertel 13y ago
The QuickCheck style of testing is my favorite (see paper [1]). Using a simple embedded DSL, you write specifications that declare the desired properties of your code. The computer then checks that the properties hold by randomly sampling the space of possible test cases, using one of several sampling strategies. Even though the checks are not proofs, they are very effective in practice. For example, here's a quick Haskell session in which I claim that the function f has the property of returning its smaller argument: Prelude> import Test.QuickCheck Prelude> let prop_minWins x y = if x < y then f x y == x else f x y == y Prelude> quickCheck prop_minWins +++ OK, passed 100 tests. The best part is that the property specifications are not only machine testable but human readable. They allow you to tell other humans what you code should do, using a clear, formal language that the machine can check to make sure you didn't tell any lies. For example, the second line in the code sample above says, "For all x and y (which are values of some type on which there is a less-than relation), if x < y then f(x, y) = x; otherwise, f(x, y) = y. See [2] for another great example. [1] http://www.eecs.northwestern.edu/~robby/courses/395-495-2009-fall/quick.pdf http://www.eecs.northwestern.edu/~robby/courses/395-495-2009... [2] http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-ParserCombinators-ReadP.html#g%3A5 http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-Pa...

farginay 13y ago

I think it is fairer to say that tests can specify a system but not to the extent that you personally want to.

colanderman 13y ago
I don't know; I'd be wary of working with any architect who handed me a list of test cases as a specification. What if he/she left out important edge cases, which I extrapolate incorrectly? How am I to infer that the absence of a test case means "not specified" vs. "specified to be the extrapolation of other test cases"? That's kind of like saying that a coder who can only write pseudocode can code a system, but not to the extent that I personally want him/her to.
- davidw 13y ago
  I'd be wary of comparing programming to architecture.
- farginay 13y ago
  Be wary of an architect who hands you anything and tells you to implement it. Real architects talk to you and sit down and write code with you.

thatthatis 13y ago

There's nothing that says any non trivial specification in any language is either complete or correct. Tests _can be_ used as a _kind of_ specification.

timtadh 13y ago
> nothing that says any non trivial specification in any language is either complete or correct. Absolutely correct. In fact the larger the specification the more likely that the specification has a bug. > Tests _can be_ used as a _kind of_ specification. Also true. But, frequently in program verification (proving a program does what it is specified to do) specifications are not tests. Why are specification not written as tests? It comes down to the program verification technique which is used. There are several categories: - Testing. "Optimistically Inaccurate" It can't find all problems but all problems it finds are real problems (assuming of course the test is correct). The downside is you may give an OK to a bad program, the upside is when you find a problem it is a real problem. - Dataflow Analysis. "Pessimistically Inaccurate" It can prove fairly general properties about a program. However, it cannot prove all properties and may not be able to prove a property which is true. For example say you where proving a program did not have a SQL injection. Dataflow analysis would OK only programs it could prove the absence of a SQL injections (as per the specification you give it! (there may be a SQL injection your spec doesn't cover)). However, there may be programs which are free of SQL injections but Dataflow Analysis is unable to prove it. - Model Checking. "Pessimistically Inaccurate, Simplified Properties" In model checking you move the program by mapping it into a new domain such as a finite state automaton. You do the mapping in such a way that properties proved about the model must hold in the actual program. Unfortunately, you can only check simplified properties and there is still some pessimistic inaccuracy (although it is reduced from dataflow analysis since the domain is easier to prove properties on). - Syntax Analysis. "Simplified Properties" Eg. Grammar Checking. You can only prove properties that can be found by a parser. You can write checks which have false positives. Eg. the check may fail but the program is fine. Type Checking is another method way as is Theorem Proving. I am sure there are even more methods beyond the ones I listed here. The point is except in the case of testing, the specifications are not given as tests. Each verification technique requires its own formal specification language. However, there are some systems where you can specify a program in a general language which can then be compiled to the verification system you actually use.

tmoertel 13y ago

The QuickCheck style of testing is my favorite (see paper [1]). Using a simple embedded DSL, you write specifications that declare the desired properties of your code. The computer then checks that the properties hold by randomly sampling the space of possible test cases, using one of several sampling strategies. Even though the checks are not proofs, they are very effective in practice. For example, here's a quick Haskell session in which I claim that the function f has the property of returning its smaller argument: Prelude> import Test.QuickCheck Prelude> let prop_minWins x y = if x < y then f x y == x else f x y == y Prelude> quickCheck prop_minWins +++ OK, passed 100 tests. The best part is that the property specifications are not only machine testable but human readable. They allow you to tell other humans what you code should do, using a clear, formal language that the machine can check to make sure you didn't tell any lies. For example, the second line in the code sample above says, "For all x and y (which are values of some type on which there is a less-than relation), if x < y then f(x, y) = x; otherwise, f(x, y) = y. See [2] for another great example. [1] http://www.eecs.northwestern.edu/~robby/courses/395-495-2009-fall/quick.pdf http://www.eecs.northwestern.edu/~robby/courses/395-495-2009... [2] http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-ParserCombinators-ReadP.html#g%3A5 http://hackage.haskell.org/package/base-4.6.0.1/docs/Text-Pa...