On Thu, Sep 27, 2012 at 12:03 PM, Nathan Ridge <zeratul976@hotmail.com> wrote:
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"?
Yeah, I was thinking more about it and maybe we can program it more or less like this: c1.resize(0); c2.clear(); assert( eq(c1, c2) ); // the actual check For every (this "for every" part is going to be hard to implement) c1 and c2 of type C and where eq returns true iff c1 and c2 are equal (eq could be implemented as operator== at least to start with). --Lorenzo