Years ago I heard an anecdote that someone had been teaching a class on verifying software. The example was proving the correctness of a sort function. For some time, the specification (thing to prove) was that the output of sort was in order. It was some time before it was realized that the spec had to be that the output was in order AND that the output was a permutation of the input.
I used this anecdote as an example that merely using "formal method" (proofs) doesn't automatically remove all errors. (Specs have to be validated.) The person I was talking to asked for a reference. I have looked and looked, but cannot find this published anywhere. If you have details about this, especially if it is in a book or article, please let me know. I hope nobody minds me posting this on the hol-info mailing list. -paul- Paul E. Black paul.bl...@nist.gov http://hissa.nist.gov/~black/ ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
