I think the confusion you're having is because in the Fibonacci example it is specifying what the Fibonacci function is by one way to calculate it. Try the following natural number division example instead. In this example the spec doesn't show how to calculate the function:

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.

A specification need not be executable.

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)

Thank you for your answer.

Is this true even for formal specifications (written in some machine-readable language)?

Couldn't you write a "compiler" for every specification written in a consistent syntax?

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.

[1]:http://sel4.systems/

Thank you for that definition. So an implementation could also be defined as a complete, machine-readable, executable specification.

Edit: Follow-up, this also means that every implementation is also a specification, right? Are there implementations that are not also specifications?

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.

[1] https://youtu.be/YoubQxqdICc?list=PLfsVAYSMwskseQbJ242TApAzA...

One possible way of seeing it, for example for a function: the specification is the table of input/output values.

The implementation is the actual code that transforms the input to the output.

There can be many different implementations for one specification.

Specifications describe what to build.

Implementation is how it is built.

There's overlap.

And there are also other design documents...sketches, plans, mockups, etc.

Thank you! Informally, this is very clear to me. But I'm asking about formal specifications here.

Formal specifications are exactly the same.

Some are entirely performance based.

Others will preclude all but a single implementation method.

And most are somewhere in-between.

Because specifications are written for a concrete context. The context solely determines what makes sense to write.

The abstractions are only abstractions. The specifications are a legal or quasi-legal obligation.