On Wednesday, 30 July 2014 at 09:13:56 UTC, Walter Bright wrote:
On 7/30/2014 12:17 AM, "Ola Fosheim Grøstad"
<ola.fosheim.grostad+dl...@gmail.com>" wrote:
[...]
This is a complete misunderstanding of what assert is. Assert
means the expression must evaluate to true, if it does not,
it's a program bug. This is the case regardless of release mode
or not.
Yes, that is my argument too. But you claim it isn't. You claim
it can be used for optimization as an annotation. Which is flat
out wrong.
This discussion will go nowhere until we both agree on what Hoare
Logic is capable of and what an annotation can be used for.
O-J. Dahl's book Verifiable Programming is my main reference
point. I read it in 3-4 days (before an exam) so it isn't too
hard, but there are probably more updated books on the topic.
Wikipedia does a fair job.
http://en.wikipedia.org/wiki/Hoare_logic
Allowing assert(0) as an annotation is like allowing
assume(true==false). Bearophile is right in disliking the
semantics and wanting halt() instead.
D would be much better off taking the direction of HAVOC:
http://research.microsoft.com/en-us/downloads/a6d296dc-e42b-4789-a720-bd3ea7b64487/
