“given a finite sequence of integers, max returns the largest of them”
“given a positive integer n, nth-twin-prime returns the n-th smallest twin prime pair, or null if no such pair exists”
Also, if a specification looks to be executable, as in your example, it need not be. It could be written in a pseudo code (https://en.wikipedia.org/wiki/Pseudocode)
If the specification is written in a machine-readable language and complete and executable then it would be an implementation.
seL4[1] is a great example of how a specification, an implementation and a formal proof system inter-work to prove an OS kernel conforms to the specs. When you read through the papers, you will see times when they found bugs in the specification.
Nothing is a specification until you label it “SPECIFICATION”, thus indicating “This is how this kind of thing is supposed to operate”.
If you do that with an implementation, you’re saying “this code has no bugs”. It may behave unexpectedly or crash, but that would all be exactly what the specification says.
Right, that makes sense, if we talk about specifications in an informal way.
Basically, any implementation I declare as specification is now a specification (Michael Scott style, heh).
But not all specifications are also implementations (at least according to this video [1]). I don't fully understand yet what makes those specifications not implementations. Maybe I need to see more examples for formal specifications that are not implementations.
Examples:
“given a finite sequence of integers, max returns the largest of them”
“given a positive integer n, nth-twin-prime returns the n-th smallest twin prime pair, or null if no such pair exists”
Also, if a specification looks to be executable, as in your example, it need not be. It could be written in a pseudo code (https://en.wikipedia.org/wiki/Pseudocode)