> nothing that says any non trivial specification in any language is either complete or correct. Absolutely correct. In fact the larger the specification the m

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