View mode: basic / threaded / horizontal-split · Log in · Help
August 01, 2010
Re: A problem with D contracts
bearophile Wrote:

> /*@ assert (\forall int i; 0 <= i && i < n; a[i] != null);
> 
This can be done with array op

assert(a[0..n].notSame(null));
August 01, 2010
Re: A problem with D contracts
Jonathan M Davis:
> IIRC TDPL, specifically mentions that contracts 
> allow for I/O for debugging purposes.

I have not yet read that part. I see print statements (and exceptions) inside contracts as something to kill with fire in my code. What's the purpose of printing stuff in contracts? Maybe Andrei is mistaken here.


> Requiring contracts to be pure would 
> destroy that ability, and there plenty of situations where that would be a big 
> problem.

See also enhancement request 3856

Bye,
bearophile
August 01, 2010
Re: A problem with D contracts
Walter Bright:
> > /*@ assert (\forall int i; 0 <= i && i < n; a[i] != null);
> 
> This does not make it simpler, it just makes things more complicated by now 
> having two ways to do a foreach.

The point here is to restrict a lot the kind of code and instructions you can put inside contracts, so eventually you will have a chance to test them automatically.

When you have copied Eiffel to design D contracts you probably have seen that in Eiffel you can't put arbitrary code inside contracts (the same is true for contract systems in C# and Java, here it's D that is designed in the wrong way). This is a limit that was there because otherwise it kills the possibility of enforcing them statically.

Bye,
bearophile
August 01, 2010
Re: A problem with D contracts
bearophile Wrote:

> because the built-in ones are not designed in a serious way, all three of them are just toys :-)

That's blasphemy! I thought you believed in D :-(
August 01, 2010
Re: A problem with D contracts
godworshipper:
> That's blasphemy! I thought you believed in D :-(

I think I lost my temper a bit while answering Jonathan, I am sorry Jonathan.

Bye,
bearophile
August 01, 2010
Re: A problem with D contracts
I agree that contracts offer too much liberty. However, I would actually 
go one step further than bearophile:

I find the need for "assert" statements not only superfluous but 
actually misleading. A contract violation is something conceptionally 
different from a broken assertion. Assertions and contracts have 
different purposes.

In my opinion, contracts should not be lists of statements but simply 
boolean expressions that have to evaluate to true. Contract checks would 
then become decoupled from assertion checks. Both could be switched 
independently at compile time.

For any case where the contract is more complex than what can be handled 
by an expression, one should simply define a pure function, which would 
even help to unclutter the code and keep contract short and concise to read.

Greetings,
Norbert


On 01/08/10 02:33, bearophile wrote:
> D contract programming lacks the 'old', but there is another different problem.
>
> Allowing only asserts (and calls to only pure/readonly functions) in precoditions, postconditions and invariants opens the door for future software that perform automatic compile-time verification of contracts.
>
> Putting all kind of D code inside contracts will make them very hard to statically verify.
>
> But simple asserts sometimes are not enough to test more complex things. So other more serious contract systems allow for asserts that contain forall, max, min, sets, and few more simple things, this is an example from a system for Java:
>
> /*@ assert (\forall int i; 0<= i&&  i<  n; a[i] != null);
>
> Beside keeping the door open to future automatic verification, that short style for conditions helps keep them shorter and less buggy (also because it helps psychological 'chunking'). If code inside contracts is long and complex then it too can contain bugs.
>
> Bye,
> bearophile
August 01, 2010
Re: A problem with D contracts
bearophile wrote:
> Walter Bright:
>> It is not easier to statically analyze a forall rather than a foreach.
> 
> The problem is that you can put any kind of code inside D contracts, this
> will make them them very to analyse automatically. The restricted semantics
> is a way to avoid this.

All it means is the analysis returns one of three states:

1. yes
2. no
3. couldn't figure it out

This is normal for static analysis. Optimizers use it extensively, for example.


>> I also see no evidence that foreach is more bug-prone than a forall would
>> be.
> 
> I have used Python lazy/eager list comps, and I think they decrease bug-count
> and speed-up coding. In the past I have explained why (mostly because of
> psychological chunking).

Supporting list comprehensions is a separate issue from whether foreach should 
be disallowed in contracts because comps are better.
August 01, 2010
Re: A problem with D contracts
bearophile wrote:
> Walter Bright:
>>> /*@ assert (\forall int i; 0 <= i && i < n; a[i] != null);
>> This does not make it simpler, it just makes things more complicated by now
>>  having two ways to do a foreach.
> 
> The point here is to restrict a lot the kind of code and instructions you can
> put inside contracts, so eventually you will have a chance to test them
> automatically.

Replacing foreach with another looping construct does absolutely nothing to 
enhance analyse-ability. You could replace them with a rat's nest of goto's and 
the compiler can still figure it out using standard, well known algorithms.

dmd's global optimizer is an example of this. In fact, all structured statements 
are reduced to if's and goto's before handing them to the optimizer, and the 
optimizer reconstructs all the loops, etc., from that flow graph. It's 1970's 
technology <g>.


> When you have copied Eiffel to design D contracts you probably have seen that
> in Eiffel you can't put arbitrary code inside contracts (the same is true for
> contract systems in C# and Java, here it's D that is designed in the wrong
> way). This is a limit that was there because otherwise it kills the
> possibility of enforcing them statically.

No, it doesn't kill it at all. It only kills it for *some* contracts.
August 01, 2010
Re: A problem with D contracts
Norbert Nemec wrote:
> I agree that contracts offer too much liberty. However, I would actually 
> go one step further than bearophile:
> 
> I find the need for "assert" statements not only superfluous but 
> actually misleading. A contract violation is something conceptionally 
> different from a broken assertion. Assertions and contracts have 
> different purposes.

In what way are their purposes different?


> In my opinion, contracts should not be lists of statements but simply 
> boolean expressions that have to evaluate to true. Contract checks would 
> then become decoupled from assertion checks. Both could be switched 
> independently at compile time.
> 
> For any case where the contract is more complex than what can be handled 
> by an expression, one should simply define a pure function, which would 
> even help to unclutter the code and keep contract short and concise to 
> read.

I think that's a stylistic issue, not a language one.
August 01, 2010
Re: A problem with D contracts
bearophile wrote:
> Jonathan M Davis:
>> IIRC TDPL, specifically mentions that contracts allow for I/O for debugging
>> purposes.
> 
> I have not yet read that part. I see print statements (and exceptions) inside
> contracts as something to kill with fire in my code. What's the purpose of
> printing stuff in contracts?

Debugging support, as mentioned in TDPL.

Being able to pepper one's code with print statements to find out where it goes 
wrong is an INCREDIBLY useful debugging technique.
1 2 3
Top | Discussion index | About this forum | D home