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

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.

I don't understand this topic well enough, so I am not saying useful things. Thank you for your comments Timon...

Bye,
bearophile

On 2013-06-15 23:50, Timon Gehr wrote:

> It bails out.

I see. That's always the problem when not using a complete compiler. Example, in my tool DStep which converts C headers to D modules it doesn't handle everything (macros and similar) but it won't bail out and continues parsing. That's because it uses a real complete compiler (Clang). So I can choose to either give an error and bail out, just skip what it cannot handle or output a comment in the translated file.

-- 
/Jacob Carlborg

On Sat, 15 Jun 2013 11:16:22 -0400, Jacob Carlborg <doob@me.com> wrote:

> On 2013-06-14 17:13, Steven Schveighoffer wrote:
>
>> With @UDAs, we have a lot of unrealized power for unit tests.
>>
>> I have asked for ModuleInfo to contain an rtInfo member [1], like
>> TypeInfo does.  With that, and possibly splitting the unit tests into
>> individual functions (if not done already, I don't know), you have all
>> you need to completely re-design the unit testing framework.  It can
>> even be runtime selectable.
>
> It would also be nice to not have to change the druntime to use RTInfo. Is that part of what you're suggesting?

No, currently RTInfo is for types only.  I want to have it work for modules as well (where unit tests typically live).

It would be nice to make it easily extensible.  I think that can be done by keying on certain members in the type/module.

-Steve

On 2013-06-17 16:21, Steven Schveighoffer wrote:

> No, currently RTInfo is for types only.  I want to have it work for
> modules as well (where unit tests typically live).

I think I understand what you mean now.

-- 
/Jacob Carlborg

On Wednesday, 12 June 2013 at 12:50:39 UTC, Andrei Alexandrescu wrote:
> Reddit: http://www.reddit.com/r/programming/comments/1g6x9g/dconf_2013_code_analysis_for_d_with_analyzed/
>
> Hackernews: https://news.ycombinator.com/item?id=5867764
>
> Twitter: https://twitter.com/D_Programming/status/344798127775182849
>
> Facebook: https://www.facebook.com/dlang.org/posts/655927124420972
>
> Youtube: http://youtube.com/watch?v=ph_uU7_QGY0
>
> Please drive discussions on the social channels, they help D a lot.
>
>
> Andrei

The website for AnalyzeD <http://analyzed.no-ip.org/> is down.  Did it get moved to somewhere else?