D enters Tiobe top 20
x at x.com
Sun Nov 10 19:14:56 UTC 2019
On Sunday, 10 November 2019 at 10:22:27 UTC, Timon Gehr wrote:
> - Modular verification means it's enough to have DI files for
> functions you call, without a function body.
In a unit testing world, every assert gets checked every time the
function is called anyhow, so it makes little difference whether
they are pre or post-conditions, or just sprinkled throughout a
In a verified world, it makes a _huge_ difference. A verified
function with an "in" contract states, "this function satisfies
all of its contracts (explicit and implicit) _if and only if_ the
in contracts/preconditions are satisfied".
With this, once that function is verified,
a caller need only make sure that it satisfies those
preconditions at each call site. In the absence of preconditions,
the verifier has to re-prove _every_ assert() in the callee
function (and every OTHER function that the callee uses too...)
_every time_ it's called throughout the program. It's an
exponential increase in the problem space.
You _might_ be able to do a flow analysis to suss out which
asserts are considered preconditions without explicitly stating
so, but it seems like a tough problem, and explicitly stating
them seems like a better practice anyhow.
Modular verification is really the only tractable way to approach
the problem. You build up the proof starting from leaf functions
which, once proven, need only their pre-conditions checked at
subsequent calls. Globals and functions with side-effects
complicate this somewhat, but for pure functions it works very
And like Timon said, in the absence of in/ out contracts in a .di
file, verified libraries provide no way to extend their
guarantees to the user.
More information about the Digitalmars-d