August 01, 2010
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
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
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
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
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
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
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
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
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
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.