Design by Contract != Runtime Assertion

[bearophile]

Walter:

> look more like math???

Right. In Spec# (and similar things are present in Eiffel, Spark and a DbC for Java) you write things like:


invariant 0 <= n && n <= a.Length;
invariant forall{int i in (n: a.Length); a[i] != key};


ensures result == exists{int x in a; x == key};


return exists{int x in a; x == key};


requires forall{int i in (0:a.Length), int j in (i:a.Length); a[i]<=a[j]};
ensures 1 <= result && result < a.Length;
ensures 0 <= result ==> a[result] == key;
ensures result == -1 ==> forall{int i in (0: a.Length); a[i] != key};


invariant forall{int i in (0: a.Length), i < low || high <= i; b[i] == a[a.Length1i]};


To me those lines look more like math formulas than normal D code.

This is useful because the contract code needs to be as much bug-free as possible, otherwise the contracts don't help. The short syntax helps the eye see that the code is correct, and having a declarative style this probably helps the analyser too. In D you need loops, sets, and other things there, that I think are less easy to analyse (because it is possible to analyse them, because commercial Lints for C are probably able to do it).


> Spec# does not do proper inheritance of preconditions (they cannot be weakened).
> It missed half of what dbc is all about with polymorphism.

It seems you and me are both blind: you see only the downsides of Spec# and I see only the good sides of it. I don't know why they have taken those decisions. Maybe to allow the static verifiability.


> C# missed the boat on polymorphic dbc completely.

They have decided that it's better to not change the C# language to add DbC to it, so they have implemented DbC as a library only (but it contains a simplified static analyser too), so I think they have had constraints.


> Spec# generates code for and checks its contracts at runtime.

Right, because there are external libs that may not use contracts, etc. But it tests the contracts at compile-time too where possible.


> And lastly, please demonstrate how:
> ...
> is not. Because I cannot figure out where you uncovered a problem.

You are right, in simple cases it's the same thing. Maybe for a good enough static analyser it's the same thing for more complex cases too, that contains nested loops, etc.

Thank you, bye,
bearophile