3

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.

  • pwparchive.wordpress.com/2012/03/29/dependent-typing-in-c - probably it's as far as you can get with C++. If you want a real dependent typing, take a look at Coq or Agda. – SK-logic Sep 27 '13 at 12:23
  • Type classes in Haskell go a long way in doing what you describe. They already define operators in terms of other operators and they can be used for user defined types as well. – Simeon Visser Sep 27 '13 at 12:25
5

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.

  • If I don't mistake that would be a non-complaint compiler only if check result was an error. If it would produce warnings, that would not be a problem for compliance... – maxim1000 Sep 27 '13 at 14:11
  • I understand it wouldn't be standard compliant, but is it possible to perform such checks in all scenarios? – ScarletAmaranth Sep 27 '13 at 15:54
  • @ScarletAmaranth - Re is it possible to perform such checks in all scenarios? No. It's an undecidable problem, the en.wikipedia.org/wiki/Entscheidungsproblem . – David Hammen Oct 1 '13 at 13:39
  • 1
    It's worthwhile to note that with types float, double, or long double, NaN < NaN is false and NaN >= NaN are both false (as are Nan < NaN, NaN >= NaN, and NaN == NaN, though curiously NaN != NaN is true. – supercat Jan 28 '14 at 16:15
0

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.

  • 1
    Key word "all". In MOST cases, on REAL code, it is trivial to determine that the code will or will not terminate, and that it does or does not meet the specification. – John R. Strohm Sep 28 '13 at 17:19
0

(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.

  • Actually, in most cases, they can. This is what static analysis is all about. I recently spent a couple of days in training on a new static analysis tool, for C. I'd previously (late 1970s) spent time on a research project on formal verification. The static analysis tool was doing a lot of what the verification tools did, over 30 years ago, and the old tools did a much better job. – John R. Strohm Sep 28 '13 at 17:21
  • @John R. Strohm: "in most cases, they can" :do you have an example or a reference for a case where the compiler can check pre- or postconditions at compiletime (and not a runtime)? – k3b Sep 28 '13 at 22:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.