checkedint call removal

via Digitalmars-d digitalmars-d at puremagic.com
Wed Jul 30 03:15:27 PDT 2014


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+dlang at 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/



More information about the Digitalmars-d mailing list