Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.

The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.

do you have a reference to anywhere that discusses this further? It seems pretty trivial to me