On Friday, 1 August 2014 at 09:02:36 UTC, Walter Bright wrote:
On 7/31/2014 11:24 PM, "Ola Fosheim Grøstad"
An assert does not say that the predicate is always true.
Yes, it does. From Meyers' comprehensive tome on the topic
"Object-Oriented Software Construction" (1997) where he writes:
"A run-time assertion violation is the manifestation of a bug
in the software."
No. Implication is not the same as equivalence.
An assert does not take a predicate. It takes a proposition that
is to be turned into a proven theorem.
bool test(bool x) {return x || !x} // predicate
test(x) for all x in {true,false} // proposition
assert(test(x) for all x in {true,false}) // prove proposition =>
proven theorem
However, you may use assumptions from a precondition locally in a
function for optimization purposes without asserting the
precondition first IFF:
1. the function is pure (no side effects)
2. the optimizer is capable of detecting inconsistencies and
ignore user provided assumptions when a conflict arises.
3. no code makes assumptions based on the postconditions of the
function
I think so, at least.
