On Wed, Oct 10, 2012 at 12:57 AM, Andrzej Krzemienski <akrzemi1@gmail.com> wrote:
P.S. I just have wild idea - what about axioms for function's arguments? i.e. not on types, but on values. Maybe some kind of axiomatic_assert. For instance that can be used to prevent pointers aliasing ("restrict" keyword in C99): void* memcpy( void* dest, const void* src, size_t count ) { axiomatic_assert( do_not_overlap(dest,src,count) ); // ... }
Is this not the same thing as preconditions in contract programming and Lorenzo's Boost.Contract library?
I think it is (of course, Boost.Contract preconditions are better because in declarations, const-correct, etc). On this topic, I still didn't give up the desire of generating preconditions from axioms and checking them at run-time. N3351 says not to do so because axioms are not constant-correct but given that axioms only alter dummy variables declared within the concepts and not in user code, I don't see why that is a problem (it'd be like allowing preconditions to declare and alter local variables, the state of the user program outside the contract code will still remain unchanged). The major issue I see so far with generating and checking preconditions from axioms is that axioms are programmed using "magic" operations like eq, <=>, is_valid, etc that cannot be implemented :( Thanks, --Lorenzo