If you have two functions implementing a different sorting algorithm, is it then possible to infer by source code that they both have the same external properties? Meaning that they both will have a possible unsorted sequence as their input and have a sorted sequence as their output? In what way could these external properties be determined by the source code? And how would you describe these external properties? What notation would be used?
The external properties could be made known by defining them explicitly, for example within a type system, but I am wondering whether this could be done implicitly. Or is it somehow theoretically impossible to infer this kind of semantics? I am interested in whether this is possible for arbitrary functions, not just for sorting algorithms, assuming things like functions will always halt and have no side-effects.
Should I look at denotational semantics, or is unrelated?
I'm interested in pointers to research in this area and to different terms used to describe the subject that might help my literature search.