I don't understand the precise difference between a specification and an implementation.
For example, in this video about formal verification [1], the person gives a recursive definition of Fibonacci as the specification:
function Fib(n: nat): nat {
if n < 2 then n else Fib(n-2) + Fib(n-1)
}
My question is now: What exactly makes the above a specification? Isn't this just another implementation (a very slow one)?
Is every specification also an implementation? Is every implementation also a specification?
From my current understanding (which is probably wrong) the answer is Yes for both.
You could say they are not the same, because specifications don't have to be complete. But to that I'd answer: many implementations are also not complete, i.e. they have undefined behavior. Isn't a specification just another implementation at a higher level of abstraction?
I just don't understand what the formal difference between the two is.
[1] Basics of specification and verification: https://www.youtube.com/watch?v=J0FGb6PyO_k&t=574s
spec: Function NatDiv implements a "division" function that given two natural numbers "dividend" and "divisor" (with the guarantees that "divisor" < "dividend" and "divisor" is not 0) either- 1) returns "quotient" an integer such that either quotientdivisor = dividend (here quotient will obviously be >=0), or, if no such number exists, returns "-1", 2) always terminates. where we assume your computer's hardware doesn't have an inbuilt division operation but has at least natural number addition, along with common comparison operations (eg: <, equality, etc) and logic ops (eg: OR, AND, NOT, etc).
Notice that here the spec doesn't specify the function by detailing what it does. In fact it specifies the division function by using multiplication which is the opposite of division. And we're not even guaranteed that our hardware has multiplication- so the spec itself gives no detail how to compute the division.
One possible NatDiv implementation: define two variables- counter and sum and set to 0. Create a while loop where the while condition to enter inside the loop is that sum is less than dividend's value. Inside the loop in each iteration sum is increased by divisor's value and counter is incremented. So when the loop terminates sum is greater than or equal to dividend's value. The function returns counter's value if sum = dividend or returns "-1" otherwise. Notice that we can argue that the loop always terminates because sum can only increase inside the loop while the value of dividend never changes thus eventually the loop condition will eventually fail to hold at some point. And when it terminates counterdivisor=sum (by the fact that multiplication of ab is equivalent to summing "a" occurrences of "b") and that counter is returned when sum=dividend or -1 is returned otherwise. Thus the requirements of the spec are satisfied.
*in reality, the spec would have to account of the size limitations of the physical machine- but here we're unrealistically assuming that it can handle any sized natural numbers.
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)
The implementation is the actual code that transforms the input to the output.
There can be many different implementations for one specification.
Implementation is how it is built.
There's overlap.
And there are also other design documents...sketches, plans, mockups, etc.