4 ms·
The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted"
by pegasus 2y ago
The program includes a lot of incidental complexity which would not be part of the spec. For example, for a sort function, the spec would be the "array sorted" postcondition. The code OTOH could be arbitrarely complex.
- zozbot234 2y agoTo be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".