Ask HN: What's the difference between a specification and an implementation?

https://news.ycombinator.com/item?id=33018665

by cloogshicer • 4 years ago

2 11 4 years ago

news.ycombinator.com

I'm a developer trying to learn more about formal methods.

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)
    }

And then they proceed to implement it with a loop, to make it actually fast and usable.

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

Someone2• 4 years ago

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)

cloogshicer4• 4 years ago

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?

GianFabien• 4 years ago

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/

brudgers2• 4 years ago

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.

cloogshicer4• 4 years ago

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

brudgers2• 4 years ago

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.

f1shy• 4 years ago

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.

haveagoodday• 4 years ago

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.

Ask HN: What's the difference between a specification and an implementation?

Related Stories