D enters Tiobe top 20
Ola Fosheim Grøstad
ola.fosheim.grostad at gmail.com
Fri Nov 8 18:25:02 UTC 2019
On Friday, 8 November 2019 at 18:11:39 UTC, Doc Andrew wrote:
> It works if you explicitly mark overflow as an error. You can
> try to prove that x <= x.max for a given path, and if you
> can't, then you just flag a warning.
So you manually assert it then? I guess you could use a templated
type with asserts builtin.
But then the solver have to figure out when to designate the type
as an integer and when to designate it as a bitvector. I guess
there is some room for that... perhaps.
Another approach is to first prove the code correct for natural
numbers and then try to prove that there is some upper limit and
select an integer size that can contain that upper limit (e.g. 64
bits vs 32 bits). I am not sure about Dafny, but I think Whiley
backends do that.
More information about the Digitalmars-d