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

[bearophile]

Timon Gehr:

> Eiffel can call arbitrary methods in contracts.

This is surprising.
Maybe the "Modern Eiffel" is more strict.


> 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. So it will give you a 
compilation error, or it will give a warning and then keep the 
contract as run-time test. In both cases this makes the static 
analysis much less useful. 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, causing those 
contracts to be not portable across static analysers. Both Ada 
and Liquid Haskell avoids all this.

Bye,
bearophile