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.
