checkedint call removal

[via Digitalmars-d]

On Wednesday, 30 July 2014 at 20:33:41 UTC, Walter Bright wrote:
>> assume(input!=0);
>>
>> If you want to specify that the input should be prevented from 
>> being zero, you
>> do this:
>>
>> if(input!=0){
>>   assert(input!=0);
>> }
>
> Now you're trying to use assert to validate user input. This is 
> a terrible, terrible misunderstanding of assert.

Can you please read the Hoare article form 1969? This is getting 
really annoying.

I am not trying to use assert to validate user input. I am 
verifying that the program is in compliance with the 
specification. Basically doing a partial proof of the theorem in 
the assert on the fly.

Example 1:

assume(x!=0) // define an axiom "x!=0"

Example 2:
if(x!=0){
    assert(x!=0) // prove theorem "x!=0" (successful)
}

Example 3:

assert(x!=0) // prove theorem "x!=0" (failure)

Example 4:

assume(x!=0); // define "x!=0" (impose constraint)
assert(x!=0); // prove theorem "x!=0" (successful)

I can't do better than this! Think of assume() as preconditions 
and assert() as postconditions.

Note also that you could use an existing theorem prover to prove 
a function correct, then machine translate it into D code with 
assume() and assert() and other machinery needed for provable 
correct programming in D.

Don't dismiss the distinction without thinking about it. Read 
Hoare's article, it is pretty well written.