D enters Tiobe top 20
Walter Bright
newshound2 at digitalmars.com
Tue Nov 12 09:12:13 UTC 2019
On 11/11/2019 8:25 PM, Doc Andrew wrote:
> I think _most_ people consider Assert vs Assume the way SPARK and F* do - as
> seen here:
> https://blogs.msdn.microsoft.com/francesco/2014/09/03/faq-1-what-is-the-difference-between-assert-and-assume/
Which says:
"Intuitively, Assert is something that you expect the static checker be able to
prove at compile time, whereas Assume is something that the static checker can
rely upon, but it will not try to prove. At runtime Assert and Assume behave the
same: If the condition is false, then the program fails – how it fails (e.g.,
throwing an exception, opening a dialog box, etc. can be completely customized
with CodeContracts)."
Therefore after the Assert, the prover can assume the Assert condition is true.
If the prover can prove the Assert is always true, the runtime check can be
safely removed.
More information about the Digitalmars-d
mailing list