"Ola Fosheim Grøstad" " wrote in message
news:[email protected]...
It follows the law of logic:
http://en.wikipedia.org/wiki/Hoare_logic
http://en.wikipedia.org/wiki/Propositional_calculus
You're missing the point - we don't have to follow those definitions. Maybe
we should - but the fact that those systems are defined that way doesn't
intrinsically mean we have to define asserts behaviour that way.
> Any verifier for D would have to understand the semantics of D's assert.
If D gets this it will be a general verifier adapted to D. That follows
the rules of established sound logic developed over the past 2300 years.
Yes, and the adaption will have to take into account D's semantics. This
doesn't mean D can't differ from other established definitions.
All asserts should be established as either true or unknown. Assert(false)
is weird. It is basically saying that true==false and asks you to prove
that over a statement/loop that may or may not terminate.
assert(false) is saying that the condition will never be met, and that
branch of execution is impossible in a correct program. (although it is
often abused to mean 'unimplemented')
