5 Oct
2012
5 Oct
'12
8:41 p.m.
Hello, 06.10.2012 0:28, Andrew Sutton wrote:
Axioms should present a consistent logical framework that precisely but generally describe the semantics our existing programs. This is not easily done.
Is it legal "to state" with axioms, something that is not true in general case? For instance, let say we have some class representing floating-point arithmetic (IEEE 754). Is it legal "to state" with axioms that it's addition operation is associative (which is not true)? If yes, then nor compiler nor any other tools MUST not do any checks on axioms besides syntactic. Best Regards, Evgeny