[pegasus]

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]

To be clear, the proper postcondition for a sort function is "the output array is a permutation of the input array and it is sorted".