Opinions on Programming by Contract
James Harris
functions to vet the input values. This has a number of benefits but
was initially included for and is especially useful for remote
procedure calls: the validation can run on the caller and thus
immediately trigger a parameter exception without the latency of
having to contact the remote process. So the sequence is
caller --> validation --> callee
where the validation is written in the callee code but where it runs
is unspecified. It can be run in the caller before the parameters
leave the caller's context.
I've just spent a couple of hours looking at Eiffel which does
something similar called Design by Contract. Under Eiffel my
construct, above, would be called a precondition. My question is:
Is it worth including in a language postconditions and class (or any
other) invariants? I'd be interested in the views of other programmers
and language designers.
--
James
Background: http://en.wikipedia.org/wiki/Design_by_contract
Presentations: http://archive.eiffel.com/doc/manuals/technology/contract/
Chris Hoare's base theory: http://en.wikipedia.org/wiki/Hoare_logic is
somewhat hard to follow, IMHO.
Jon Harrop
> Is it worth including in a language postconditions and class (or any
> other) invariants? I'd be interested in the views of other programmers
> and language designers.
My impression is that "design by contract" is nothing more than a new name
for an ancient idea: assertions. I prefer to keep production code clean so
I separate tests from the implementations. Also, I value a decent static
type system (e.g. OCaml, F#, Haskell, SML) vastly more than design by
contract.
--
Dr Jon D Harrop, Flying Frog Consultancy
http://www.ffconsultancy.com/products/?u
cbcurl
> James Harris wrote:
> > Is it worth including in a language postconditions and class (or any
> > other) invariants? I'd be interested in the views of other programmers
> > and language designers.
>
> My impression is that "design by contract" is nothing more than a new name
> for an ancient idea: assertions. I prefer to keep production code clean so
> I separate tests from the implementations. Also, I value a decent static
> type system (e.g. OCaml, F#, Haskell, SML) vastly more than design by
> contract.
DbC is a form of assertion checking but with language and runtime
environment support to make it easier to express certain OO assertions
such as class invariants, and method preconditions and
postconditions. For instance, if a postcondition of a method must
also be honored by all overridden versions of that method in
subclasses. Writing these kinds of assertions by hand can be onerous,
so it is useful to have some support from your language and
development environment.
Static type systems only replace the aspects of DbC that are related
to type checking. It's not really an either-or comparison.
While it is nice to separate code and tests/assertions, you can only
do this if your language runtime provides some way break class
encapsulation (e.g. provide external access to private members) and
provides some sort of aspect-oriented programming model to be able to
hook external assertions into the code at runtime.
In languages with conditional compilation you can wrap your assertion
checking code using macros to prevent code bloat in production.
scholz...@gmail.com
> Static type systems only replace the aspects of DbC that are related
> to type checking. It's not really an either-or comparison.
Yes i found it most effective when i use some state machine in my
classes
and assert that methods are called in valid sequence.
Also you forgot to mention the huge benefit on documentation. Even a
set_name (s: STRING) is
require
s /= Void
do
ensure
name = s
end
gives you a good information: That the string is not copied but simply
referenced
(strings in eiffel are mutable and therefore dangerous).
> While it is nice to separate code and tests/assertions, you can only
> do this if your language runtime provides some way break class
> encapsulation (e.g. provide external access to private members) and
> provides some sort of aspect-oriented programming model to be able to
> hook external assertions into the code at runtime.
To be honest i don't like all this aspect oriented stuff. Its much
better
if you see the assertions in place.
And to the OP. I find postconditions very usefull and use them often.
I almost never use class invariants for the simple fact that they are
very expensive in terms of runtime and the currently existing
compilers
do not offer an easy way to eliminate the ones you don't want to
check.
But this is only a very pragmatic reason, i think they can be of good
help.
Malcolm McLean
"James Harris" <james.h...@googlemail.com> wrote in message news:
> Is it worth including in a language postconditions and class (or any
> other) invariants? I'd be interested in the views of other programmers
> and language designers.
>
variables.
eg
int i <0, N-1> /* i is a counter */
you can extend this idea to input parameters and the return value. Obviously
things get a bit trickier when you pass in vectors or structures.
--
Free games and programming goodies.
http://www.personal.leeds.ac.uk/~bgy1mm
Jussi Säntti
> My language design includes a "validation" section at the top of
> functions to vet the input values. This has a number of benefits but
> was initially included for and is especially useful for remote
> procedure calls: the validation can run on the caller and thus
> immediately trigger a parameter exception without the latency of
> having to contact the remote process. So the sequence is
>
> caller --> validation --> callee
>
> where the validation is written in the callee code but where it runs
> is unspecified. It can be run in the caller before the parameters
> leave the caller's context.
This is the seldom discussed connection between DbC and RPC. Reason is most
DbC people thinking RPC is not good for remoting. Compiler support of DbC is
essentially making the assertions separate from the body of the routine.
Various flavors of IDL is one place where the interface is separate from the
body. Now one can wonder why contracts were not supported in Corba, COM etc
and still not in the binary IDL of .NET.
Jon Harrop
> DbC is a form of assertion checking but with language and runtime
> environment support to make it easier to express certain OO assertions
> such as class invariants, and method preconditions and
> postconditions. For instance, if a postcondition of a method must
> also be honored by all overridden versions of that method in
> subclasses. Writing these kinds of assertions by hand can be onerous,
> so it is useful to have some support from your language and
> development environment.
>
> Static type systems only replace the aspects of DbC that are related
> to type checking. It's not really an either-or comparison.
That may be true in theory but, in practice, languages supporting design by
contract do not have decent static type systems. So it is very much an
either-or comparison.
> While it is nice to separate code and tests/assertions, you can only
> do this if your language runtime provides some way break class
> encapsulation (e.g. provide external access to private members) and
> provides some sort of aspect-oriented programming model to be able to
> hook external assertions into the code at runtime.
Assuming OOP, yes. Otherwise, better solution exist (and predate AOP).
James Harris
Widening the net a bit to include comp.lang.eiffel. Presumably folks
there like all three parts of the DbC feature. There are other
comments (currently six replies) in the original groups in case anyone
from c.l.e want to see them and agree with or rail against them!
I can't help wondering if there are other places where asserts should/
could be used. Perhaps Chris Hoare's base theory just proposes these.
In fact pre and post conditions may be all that's required by the
theory. The invariants automatically apply at both times.
--
James
James Harris
> "James Harris" <james.harri...@googlemail.com> wrote in message news:
> > Is it worth including in a language postconditions and class (or any
> > other) invariants? I'd be interested in the views of other programmers
> > and language designers.
>
> If you're writing a high-level language, it's worth including ranges for
> variables.
>
> eg
>
> int i <0, N-1> /* i is a counter */
>
> you can extend this idea to input parameters and the return value. Obviously
> things get a bit trickier when you pass in vectors or structures.
Interesting. I am tenuously thinking of the compiler maintaining
possible range information as it looks at the dynamic flow of
computation. This is for optimisation purposes.
I am torn between checking and not checking actual variable ranges for
performance reasons. I can see that if I allow pre and post assertions
this is a natural extension, i.e. an invariant on a variable
declaration which, I believe is not supported in Eiffel (as Eiffel
only allows on new object types) but I may be wrong.
Speaking of language design and performance there may be a tie-in
between variable ranges and the saturated arithmetic performed by
Intel/AMD CPUs. In this case, a sum exceeding the limit would be
_silently_ pegged back to the limit. I presume preconditions and
postconditions are normally expected to raise an exception if the
condition is violated. Hmm....
--
James
cbcurl
> cbcurl wrote:
> > Static type systems only replace the aspects of DbC that are related
> > to type checking. It's not really an either-or comparison.
>
> That may be true in theory but, in practice, languages supporting design by
> contract do not have decent static type systems. So it is very much an
> either-or comparison.
I think that is a silly claim to make unless you are willing to
explain exactly what you mean. What specifically is wrong with
Eiffel's static type system?
> > While it is nice to separate code and tests/assertions, you can only
> > do this if your language runtime provides some way break class
> > encapsulation (e.g. provide external access to private members) and
> > provides some sort of aspect-oriented programming model to be able to
> > hook external assertions into the code at runtime.
>
> Assuming OOP, yes. Otherwise, better solution exist (and predate AOP).
And these better solutions are...?
Jon Harrop
> On Jun 18, 2:51 am, Jon Harrop <j...@ffconsultancy.com> wrote:
>> cbcurl wrote:
>> > Static type systems only replace the aspects of DbC that are related
>> > to type checking. It's not really an either-or comparison.
>>
>> That may be true in theory but, in practice, languages supporting design
>> by contract do not have decent static type systems. So it is very much an
>> either-or comparison.
>
> I think that is a silly claim to make unless you are willing to
> explain exactly what you mean. What specifically is wrong with
> Eiffel's static type system?
Eiffel has no algebraic data types, no function types (no higher-order
functions), no higher-order module types, no structural types, no automatic
generalization of types, no pure types, no linear types...
This is not surprising given that Eiffel is over 20 years out of date: it
predates the theory that underpins all modern static type systems.
Consequently, its rudimentary static type system is unable to convey even
the most basic of constraints and Eiffel developers have no choice but to
resort to design by contract. Conversely, programmers using languages with
powerful static type systems have no need of design by contract: it is just
a source of unwanted run-time errors.
>> > While it is nice to separate code and tests/assertions, you can only
>> > do this if your language runtime provides some way break class
>> > encapsulation (e.g. provide external access to private members) and
>> > provides some sort of aspect-oriented programming model to be able to
>> > hook external assertions into the code at runtime.
>>
>> Assuming OOP, yes. Otherwise, better solution exist (and predate AOP).
>
> And these better solutions are...?
Higher-order module systems.
Peter Hermann
> This is not surprising given that Eiffel is over 20 years out of date: it
> predates the theory that underpins all modern static type systems.
> Consequently, its rudimentary static type system is unable to convey even
> the most basic of constraints and Eiffel developers have no choice but to
> resort to design by contract. Conversely, programmers using languages with
> powerful static type systems have no need of design by contract: it is just
> a source of unwanted run-time errors.
moreover, Eiffel is proprietary ( as well as F# (-:sorry:-) )
Ada is open source:
https://libre.adacore.com/
http://www.ihr.uni-stuttgart.de/forschung/ada/resources_on_ada/
BTW compliment for great page F#:
http://www.ffconsultancy.com/products/?u
cbcurl
> cbcurl wrote:
>
> > I think that is a silly claim to make unless you are willing to
> > explain exactly what you mean. What specifically is wrong with
> > Eiffel's static type system?
>
> Eiffel has no algebraic data types, no function types (no higher-order
> functions), no higher-order module types, no structural types, no automatic
> generalization of types, no pure types, no linear types...
Yes, but how does that make it's type system not "decent"? How many
languages do have all those kinds of types and how many programmers
actually use such languages? And what do any of those types have to do
with the type of assertions that real people write. For instance, it
is quite common to write precondition assertions for internal
implementation methods that check for various states of class members.
Friedrich Dominicus
> Peter Hermann <ica...@lucky.ihr.uni-stuttgart.de> writes:
>>Eiffel is proprietary
>
> Does this refer to
>
> - the rights to use the name »Eiffel« for a programming-related
> product,
I guess the rights are on the name are with ISE
>
> - the status of the specification of this language »Eiffel«, or
Hm, AFAIKT there is en EMCA standard, so everyone should be "allowed"
to make his /her implementation
>
> - the status of the single implementation of this language
> »Eiffel«, or
there is a family of Eiffel related languages out there. So we hardly
can speak of a single implementation.
>
> - the status of every implementation of this language »Eiffel«,
> or
>
> - patents making it impossible to publish a free implementation
> of it, or
no
>
> - a mixture of the above or something else?
I don't know AFAIKT both ISE Eiffel and SmartEiffel are under the GPL
partly. So I can not see where the proprietary comes from
Regards
Friedrich
--
Please remove just-for-news- to reply via e-mail.
Jon Harrop
> On Jun 19, 2:01 am, Jon Harrop <j...@ffconsultancy.com> wrote:
>> cbcurl wrote:
>> > I think that is a silly claim to make unless you are willing to
>> > explain exactly what you mean. What specifically is wrong with
>> > Eiffel's static type system?
>>
>> Eiffel has no algebraic data types, no function types (no higher-order
>> functions), no higher-order module types, no structural types, no
>> automatic generalization of types, no pure types, no linear types...
>
> Yes, but how does that make it's type system not "decent"?
Those features allow you to convey far more information to the compiler for
static checking. That is intimately related to run-time checking using
assertions. You should always opt for static checking of constraints when
possible.
> How many languages do have all those kinds of types and how many
> programmers actually use such languages?
I would estimate ~100k such programmers. Moreover, statically-typed
functional programming languages are by far the fastest growing sector of
programming languages. Uptake has been quadrupling every year for four
years now and Microsoft recently announced the productization of their own
statically-typed functional language for .NET: F#.
> And what do any of those types have to do
> with the type of assertions that real people write. For instance, it
> is quite common to write precondition assertions for internal
> implementation methods that check for various states of class members.
You might write an assertion to check that a list argument is never empty.
Tuples and algebraic data types let you convey the same information to the
compiler for static verification: removing those assertions and, more
importantly, removing all subsequent source of run-time error.
Friedrich Dominicus
> I would estimate ~100k such programmers. Moreover, statically-typed
> functional programming languages are by far the fastest growing sector of
> programming languages. Uptake has been quadrupling every year for four
> years now and Microsoft recently announced the productization of their own
> statically-typed functional language for .NET: F#.
100 -> 400 -> 1600 -> 6400
Yepp, I guess you could be right ;-)
Astonishingly figures
Have a nice day
Greg Herlihy
wrote:
> In comp.lang.misc Jon Harrop <j...@ffconsultancy.com> wrote:
>
> moreover, Eiffel is proprietary ( as well as F# (-:sorry:-) )
Eiffel is an ISO Standard, like C or C++.
> Ada is open source:https://libre.adacore.com/http://www.ihr.uni-stuttgart.de/forschung/ada/resources_on_ada/
So I take it that the primary advantage of "open-sourcing" a
programming language is that programmers using the language do not
have to wait (sometimes for years) on some group of people in some
organization somewhere in Switzerland - to sober up long enough to
make some needed improvements to the lanuguage. Instead, with an open-
sourced language, each programmer is encouraged to make their own
language enhancements - and is free to do so in whatever way best
suits their individual taste in programming languages.
Greg
Jon Harrop
> Jon Harrop <j...@ffconsultancy.com> writes:
>> I would estimate ~100k such programmers. Moreover, statically-typed
>> functional programming languages are by far the fastest growing sector of
>> programming languages. Uptake has been quadrupling every year for four
>> years now and Microsoft recently announced the productization of their
>> own statically-typed functional language for .NET: F#.
> Let's see
> 100 -> 400 -> 1600 -> 6400
>
> Yepp, I guess you could be right ;-)
6,400 != 100,000