Can compilers check whether certain axioms hold for a user defined type?

Question

Suppose the following type is defined (C++ syntax, can be conceptually applied to any statically typed language.)

class T {
   int val;
   friend bool operator<(const T& lhs, const T& rhs) {
      return lhs.val < rhs.val;
   }
   // Ideally, if we should make them "friends"
   // Also, this doesn't make them belong to the type itself as they're not member functions
   friend bool operator>=(const T& lhs, const T& rhs) {
      return !(lhs < rhs);
   }
   // Also the following implementation is interesting
   friend bool operator>=(const T& lhs, const T& rhs) {
      return lsh.val >= rhs.val;
   }
};

So, the compiler can definitely check whether T supports operator< or operator>=, it can just look up the declaration.
This gets more complicated should these be defined as "friends" instead of member functions, but it can be done as far as I'm concerned.

However, can the compiler check whether the "common axiom of sorts" hold? (Can as in is it possible to check this in all scenarios? Doesn't matter whether or not this would be standard-compliant.) Say:
not (a < b) == a >= b

Should we define one in terms of the other, it is definitely possible in this particular scenario, but this is naturally not the only axiom that needs to be checked, what about:
(a > b) => (b < a)
and it's also not necessary (unfortunately) to define our behaviour in terms of something that has already been defined. And sometimes it wouldn't be even possible.

So, if the compiler can check whether certain axioms hold, how? Generating random values from certain ranges? Is it possible to devise and proof correctness of such ranges?

This is mainly related to C++ concepts that unlike C++ concepts lite, should also be able to "support axioms", whatever that means, I just can't see a clear way as to how they can be enforced. Or will the creator of the type have to state what axioms his class obeys? C++ dropped the "concept maps" as far as I know.

Answer 1

However, can the compiler check whether the "common axiom of sorts" hold?

No. That would be a non-compliant compiler. There's nothing in the standard that says that, for example, operator>= must be the boolean inverse of operator<. It's perfectly okay per the standard if a programmer wants to define all of the comparison operators as return 42;. That this is not a good idea is a different question.

The compiler has a hard enough time already given the complexity of C++. It's not a good idea to add a Sysiphean task to that load. Your 'testing of axioms' is in general an undecidable problem.

Answer 2

No. Since the operators can hold arbitrary code, it is impossible to even determine whether they will terminate in all instances. For more info on this, look up the halting problem.

Answer 3

(Note This answer is based on experience in c#. I have never tried it in c/c++)

I don-t think, pre- or postcoditions (like sorting) can be checked at compiletime at all.

But a compiler (or a compiler-postprocesser) can automatically insert code to do runtimechecks for pre- and postconditions. (That is the way it is done in c# code contracts which make shure that contracts are also enforced in overwritten virtual functions, too.

Wikipedia lists under Design_by_contract some c/c++ libraries to support contracts.

UML uses OCL=Object_Constraint_Language for this.