DConf 2013 Day 3 Talk 2: Code Analysis for D with AnalyzeD by Stefan Rohe

[Timon Gehr]

On 06/16/2013 12:07 AM, bearophile wrote:
> Timon Gehr:
>
>> Eiffel can call arbitrary methods in contracts.
>
> This is surprising.
> Maybe the "Modern Eiffel" is more strict.
>

It's design isn't finished, but IIRC it enforces purity, contracts can 
be arbitrarily complex, and manual proofs are required.

>
>> I disagree. The only problem is the verboseness of the contract system.
>
> If your contracts contain arbitrary D code, I don't think a static
> analyser will be able to use them.

Why not? The static analyser obviously needs to analyse arbitrary D code 
anyway, unless it only analyses contracts, which is not useful.

> So it will give you a compilation
> error, or it will give a warning and then keep the contract as run-time
> test.

It's unreasonable to expect that the static analyser will automatically 
prove all correct programs correct without manually provided evidence. 
This holds true independently of the format the contracts are specified in.

> In both cases this makes the static analysis much less useful.

Than what?

> So you end using a subsed of the D syntax and D semantics. But then
> compilation becomes a try-and-guess, and different static analysers will
> digest different amounts of D syntax and semantics,

Obviously. But not closely related to the way contracts are specified.

> causing those contracts to be not portable across static analysers.

If those analysers all follow the same specification, they will be 
portable in any case.

> Both Ada

Reference?

> and Liquid Haskell avoids all this.
> ...

It does not make any sense to claim that Liquid Haskell avoids all this.
It is not a programming language but a static verifier, AFAIK based on 
predicate abstraction.