David Crocker wrote:
For years, I have been trying to get formal specification advocates to explain the difference between high level programming languages and specification languages. From my point of view, "formal specifications" can be divided into two categories:Crispin Cowan wrote:
The above is the art of programming language design. Programs written in
high-level languages are *precisely* specifications that result in the
system generating the program, thereby saving time and eliminating
coding error. You will find exactly those arguments in the preface to
the K&R C book.
<<
Whilst I agree that the distinction between specification and programming
languages is not completely clear cut, there is nevertheless a fundamental
difference between specification and programming.
* Those that can be mechanically translated into code, otherwise
known as "programs"
* Those that cannot be mechanically translated, otherwise known as
"documentation" :)In a programming language, you tell the computer what you want it to do,I agree with the other posters: the above could describe a formal specification, but could also describe a declarative programming language.
normally by way of sequential statements and loops. You do not tell the computer
...
In a specification language, you tell the computer what you are trying to
achieve, not how to achieve it. This is typically done by expressing the desired
relationship between the input state and the output state. The state itself is
normally modelled at a higher level of abstraction than in programming (e.g. you
wouldn't refer to a hash table, because that is implementation detail; you would
refer to a set or mapping instead).
However, I think I do see a gap between these extremes. You could have a formal specification that can be mechanically transformed into a *checker* program that verifies that a solution is correct, but cannot actually generate a correct solution. The assert() statements that David Crocker mentioned are an incomplete form of this; incomplete because the do not *completely* verify the program's behavior to be correct (because they are haphazardly placed by hand).
So there's another midpoint in the spectrum: a formal spec that can only verify correctness but is complete, effectively is a program for non-deterministic machines (cf: NP completeness theory). A spec that is incomplete (does not specify all outputs) is more of an approximation.
All of which begs the question: are these formal specs that are somehow not programs any easier to verify than actual programs? Probably somewhat easier (they are necessarily simpler) but some would argue, not enough simpler to be worth the bother. E.g. suppose 100,000 lines of code reduces to 10,000 lines of formal specification in some logical notation. A hard problem, but solvable, is a mechanical proof that the 10,000 line spec and the 100,000 lines of code actually conform. An unsolved problem is "does the 10,000 line spec mean what the human *thinks* it means?"
Crispin
-- Crispin Cowan, Ph.D. http://immunix.com/~crispin/ CTO, Immunix http://immunix.com
