Re: [boost] [contract] toward N3351 concepts

Subject: Re: [boost] [contract] toward N3351 concepts
From: Nathan Ridge (zeratul976_at_[hidden])
Date: 2012-09-27 15:03:54

> Again, I'm learning these things as we go... but aren't => and <=> the
> "implies" and "if and only if" logical operators? If so, their operand
> must be boolean predicates so I don't understand what this axioms
> means:
> 
> c.resize(0) <=> c.clear()
> 
> Oh, I see, <=> is some sort of magic "equivalence" operator as it can
> be defined only meta+programmatically in the programmer's mind. This
> axiom means that "the effect of c.resize(0) must be /equivalent/ to
> c.clear()" in a way that the program will never be able to assert. I
> can't even check that syntactically, can I? What does it mean to check
> the axiom above syntactically given that I'd have to completely strip
> away the <=> operator because it cannot be represented
> programmatically? Then such an axiom is just a code comment and maybe
> it should be programmed as such IMO.

Perhaps we can interpret this formally as "all the variables that appear
in both expressions [in this case, c] compare equal after the expressions
are evalauted"?

Regards,
Nate