3 ms·
A specification isn't the same as executable code. For example, the specification for sorting any array A having indexes [0 .. n) is the resulting array B such
by nayuki 5y ago
A specification isn't the same as executable code. For example, the specification for sorting any array A having indexes [0 .. n) is the resulting array B such that there exists a permutation P of [0 .. n) such that B[P(0)] <= B[P(1)] <= ... <= B[P(n-1)]. But this specification says nothing about how to find such a permutation. You could do it by brute force because the space is finite, but that wouldn't be a practical sorting algorithm. So a practical algorithm will have a different flavor and different proof than the simplest specification.
- Mikhail_Edoshin 5y agoIt looks like too big a specification, more like a wish. We could equally well write that the result must be a solution to the traveling salesman problem. A specification can only be useful if there exist a piece of code that can take it, apply it to the algorithmic part and tell us the results. I'm thinking more along the lines of "when this field is X, that field can only be Y or Z" or "when this condition holds, these fields are not accessed". And these declarations should be a part of the main code so that it can refer to its internals.