This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Design By Contract

33 replies
Jann Röder
Joined: 2010-07-08,
User offline. Last seen 42 years 45 weeks ago.

I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann

David Pollak
Joined: 2008-12-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

Thanks,

David

On Thu, Jul 8, 2010 at 8:05 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann






--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics
Dean Wampler
Joined: 2008-12-26,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract
I'm an old DbC fan, too, having used it very successfully years ago in C. I even wrote a DbC tool for Java (http://contract4j.org), which is now somewhat dated. 
We discussed DbC briefly in Programming Scala: http://programming-scala.labs.oreilly.com/ch13.html#DesignByContractExample
I agree with David that I try to use the type system, along with tests, to achieve the same goals. I'm not sure I would advocate adding DbC to Scala itself, although a compiler plugin, if possible, would be very interesting. (Master's thesis project??)
dean

On Thu, Jul 8, 2010 at 10:57 AM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

Thanks,

David

On Thu, Jul 8, 2010 at 8:05 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann






--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics



--
Dean Wampler
"Programming Scala" (O'Reilly)  http://programmingscala.com
twitter: @deanwampler, @chicagoscala
http://polyglotprogramming.com

Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract
I highly suggest looking at the Code Contracts Microsoft research project:
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Essentially, you would introduce your contract code in the "traditional" way - that is coding pre-conditions/post-conditions/assertions as part of the implementation, more or less as it has traditionally been done.

The inheritance of code contracts is implemented via bytecode transformation, so there is no need for language support for this feature. Also, support for code contracts was added to the sandcastle documentation generation tool, so that you can document pre/post-conditions as part of the "interface" to your library.

What really makes Code Contracts stand out, however, is that along with the run-time library which checks for contract violations at run-time, there is a static analysis engine that statically checks code for violations, or possible violations of code contracts, essentially at compile time (technically, shortly after compile time, as a post-process step).

The main obstacle of implementing something like this in scala is just the relative complexity of the scala type system as compared to .net, which would make it more difficult to implement the bytecode transformation required to implement contract inheritance, and of course the static analysis engine for verifying code contracts at compile time. This is especially true considering that the static analysis engine is, I assume, already somewhat sophisticated.

On Thu, Jul 8, 2010 at 11:57 AM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

Thanks,

David

On Thu, Jul 8, 2010 at 8:05 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann






--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics

Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract
I should also mention that Code Contracts was not meant as an alternative to unit testing. In fact, Microsoft Research's PEX project (a "parametrized" unit testing framework) shows that combining the two methods can be extremely powerful:

http://microsoftpdc.com/Sessions/VTL01



On Thu, Jul 8, 2010 at 12:56 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
I highly suggest looking at the Code Contracts Microsoft research project:
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Essentially, you would introduce your contract code in the "traditional" way - that is coding pre-conditions/post-conditions/assertions as part of the implementation, more or less as it has traditionally been done.

The inheritance of code contracts is implemented via bytecode transformation, so there is no need for language support for this feature. Also, support for code contracts was added to the sandcastle documentation generation tool, so that you can document pre/post-conditions as part of the "interface" to your library.

What really makes Code Contracts stand out, however, is that along with the run-time library which checks for contract violations at run-time, there is a static analysis engine that statically checks code for violations, or possible violations of code contracts, essentially at compile time (technically, shortly after compile time, as a post-process step).

The main obstacle of implementing something like this in scala is just the relative complexity of the scala type system as compared to .net, which would make it more difficult to implement the bytecode transformation required to implement contract inheritance, and of course the static analysis engine for verifying code contracts at compile time. This is especially true considering that the static analysis engine is, I assume, already somewhat sophisticated.

On Thu, Jul 8, 2010 at 11:57 AM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

Thanks,

David

On Thu, Jul 8, 2010 at 8:05 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann






--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics


extempore
Joined: 2008-12-17,
User offline. Last seen 35 weeks 3 days ago.
Re: Design By Contract

On Thu, Jul 08, 2010 at 01:00:59PM -0400, Jeremy Bell wrote:
> I should also mention that Code Contracts was not meant as an
> alternative to unit testing. In fact, Microsoft Research's PEX project
> (a "parametrized" unit testing framework) shows that combining the two
> methods can be extremely powerful:
>
> http://microsoftpdc.com/Sessions/VTL01

You might want to look at martin's comments in this thread:

http://www.scala-lang.org/node/5700#comment-23437

I agree there is goodness to be had. I think bytecode rewriting should
be an absolute last resort though.

Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract
Dear Jann,
In the not too distant future behavioral typing will be added to the richness one currently finds in type systems for functional languages. 
That said, i wouldn't add something like this to a language like Scala or Haskell where the core abstraction is fundamentally sequential (cf Berry's sequentiality theorem). (Though, i am sorely tempted to add it to a Scala-based DSL.)
i believe that in the not too distant future we will have more than one language candidate in which the core abstraction is fundamentally concurrent (cf, π-calculus, ambient calculus, etc). These will more or less necessitate behavioral types. With behavioral types a useful and compiler-supported design-by-contract capability will essentially be realized by the type system.
Best wishes,
--greg

On Thu, Jul 8, 2010 at 10:00 AM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
I should also mention that Code Contracts was not meant as an alternative to unit testing. In fact, Microsoft Research's PEX project (a "parametrized" unit testing framework) shows that combining the two methods can be extremely powerful:

http://microsoftpdc.com/Sessions/VTL01



On Thu, Jul 8, 2010 at 12:56 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
I highly suggest looking at the Code Contracts Microsoft research project:
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Essentially, you would introduce your contract code in the "traditional" way - that is coding pre-conditions/post-conditions/assertions as part of the implementation, more or less as it has traditionally been done.

The inheritance of code contracts is implemented via bytecode transformation, so there is no need for language support for this feature. Also, support for code contracts was added to the sandcastle documentation generation tool, so that you can document pre/post-conditions as part of the "interface" to your library.

What really makes Code Contracts stand out, however, is that along with the run-time library which checks for contract violations at run-time, there is a static analysis engine that statically checks code for violations, or possible violations of code contracts, essentially at compile time (technically, shortly after compile time, as a post-process step).

The main obstacle of implementing something like this in scala is just the relative complexity of the scala type system as compared to .net, which would make it more difficult to implement the bytecode transformation required to implement contract inheritance, and of course the static analysis engine for verifying code contracts at compile time. This is especially true considering that the static analysis engine is, I assume, already somewhat sophisticated.

On Thu, Jul 8, 2010 at 11:57 AM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

Thanks,

David

On Thu, Jul 8, 2010 at 8:05 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
I searched the mailing list archive and I could not find a discussion
about Design by Contract in Scala.

So my question is, if Design by Contract has been or is being considered
for inclusion in a future version of Scala and if not, why not. I know
there are some libraries that try to implement DbC as a library but I
think they are missing a very important point: Contracts are part of the
method signature or class interface and not of the implementation.
Therefore contracts are also inherited and this is not possible without
language support.

Scala is a really great language and for sure much more powerful and
expressive than Java. Its functional programming features would allow
developers to write very concise and expressive contracts. I have found
design by contract to greatly reduce debugging time and lead to less
bugs in my software in general. So in my opinion the addition of DbC to
Scala would make an already great language almost perfect.

On a related note:
I like the fact that Scala does away with Java-style checked exceptions.
As suggested by this slightly outdated paper
(http://www.springerlink.com/content/264g7772m8237180/) the use of
contracts seems to greatly reduce the need for exceptions.

I'm curious about your opinions.
Jann






--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics





--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com
Jann Röder
Joined: 2010-07-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract

> Coming to Scala, I found that a lot of the stuff that I did with DbC >
could be done with the type system. And when it's done with the type >
system, it's compile-time enforced and it's more obvious to the
> library consumer what the constraints are.

Unless I'm missing something the only "contract" you can enforce with
the type system is that an argument or return values is not null. You
are probably referring to the Option class here since Scala's
non-nullable types don't seem to be ready yet. The Eiffel compiler has
introduced void-safety about two years ago and there are still open
problems. For something like that to really work the entire base library
must support it - which is far from trivial (e.g. Arrays).

Of course I don't consider things like "the argument must be of type X"
a contract.

> I highly suggest looking at the Code Contracts Microsoft research
> project:

After reading this quite interesting paper:
http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own...
I think that the code contracts project is what the Spec# people could
rescue over into the production .NET framework. Spec# is dead now and
they did not want to really introduce contracts into C#. I also conclude
that static verification of code contracts will always be very limited
in "normal" programming languages. The spec# people had to introduce
lots of annotations to help the verifier. This is of course not
practical for a non-research language.

On the other hand interface contracts with runtime verification have
proven to be useful and practical in Eiffel over many years and I really
wonder why no other language (except maybe D) supports it.

Also note that as least as important as runtime verification is the
self-documentation aspect of code contracts. And for this documentation
aspect it is important for the contracts to be part of the method
signature and not the body.

Bytecode transformation is only a hack if you do not want to change the
language anymore - but since Scala is still evolving it might still be
possible to add it as a language feature...

Jann

Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract
Dear Jann, et al,
Apropos of this thread, my friends and colleagues, Laura Bocchi, Kohei Honda and Nobuko Yoshida, just got a paper into Concur discussion the relationship of DbC and behavior types.
Best wishes,
--greg

On Thu, Jul 8, 2010 at 10:47 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
> Coming to Scala, I found that a lot of the stuff that I did with DbC >
could be done with the type system.  And when it's done with the type >
system, it's compile-time enforced and it's more obvious to the
> library consumer what the constraints are.

Unless I'm missing something the only "contract" you can enforce with
the type system is that an argument or return values is not null. You
are probably referring to the Option class here since Scala's
non-nullable types don't seem to be ready yet. The Eiffel compiler has
introduced void-safety about two years ago and there are still open
problems. For something like that to really work the entire base library
must support it - which is far from trivial (e.g. Arrays).

Of course I don't consider things like "the argument must be of type X"
a contract.

> I highly suggest looking at the Code Contracts Microsoft research
> project:

After reading this quite interesting paper:
http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own&id=BarnettEA10.pdf
I think that the code contracts project is what the Spec# people could
rescue over into the production .NET framework. Spec# is dead now and
they did not want to really introduce contracts into C#. I also conclude
that static verification of code contracts will always be very limited
in "normal" programming languages. The spec# people had to introduce
lots of annotations to help the verifier. This is of course not
practical for a non-research language.

On the other hand interface contracts with runtime verification have
proven to be useful and practical in Eiffel over many years and I really
wonder why no other language (except maybe D) supports it.

Also note that as least as important as runtime verification is the
self-documentation aspect of code contracts. And for this documentation
aspect it is important for the contracts to be part of the method
signature and not the body.

Bytecode transformation is only a hack if you do not want to change the
language anymore - but since Scala is still evolving it might still be
possible to add it as a language feature...

Jann




--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com
Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract
On Thu, Jul 8, 2010 at 1:47 PM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
> Coming to Scala, I found that a lot of the stuff that I did with DbC >
could be done with the type system.  And when it's done with the type >
system, it's compile-time enforced and it's more obvious to the
> library consumer what the constraints are.

Unless I'm missing something the only "contract" you can enforce with
the type system is that an argument or return values is not null. You
are probably referring to the Option class here since Scala's
non-nullable types don't seem to be ready yet. The Eiffel compiler has
introduced void-safety about two years ago and there are still open
problems. For something like that to really work the entire base library
must support it - which is far from trivial (e.g. Arrays).

Of course I don't consider things like "the argument must be of type X"
a contract.

 I am also confused as to how scala's type system could be used as a replacement for generalized contracts (in other words, anything beyond simple "parameter is non-null" or "return value is non-null" type contracts). Maybe someone could give an example? I would be curious to see this.

 
> I highly suggest looking at the Code Contracts Microsoft research
> project:

After reading this quite interesting paper:
http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own&id=BarnettEA10.pdf
I think that the code contracts project is what the Spec# people could
rescue over into the production .NET framework. Spec# is dead now and
they did not want to really introduce contracts into C#. I also conclude
that static verification of code contracts will always be very limited
in "normal" programming languages. The spec# people had to introduce
lots of annotations to help the verifier. This is of course not
practical for a non-research language.

I disagree that code contracts are not practical for a non-research language. I have used Code Contracts in my own projects, and while I found it took some non-trivial work introducing contracts to an existing code-base (and there were a few confusing warnings that were generally addressed by introducing Assumptions), once the contracts were in place and I was writing contracts for any new code, the overhead was negligible, especially considering the benefits.

Also, scala's syntax could possibly allow for more succinct definition of contracts than is possible in C#.
 
On the other hand interface contracts with runtime verification have
proven to be useful and practical in Eiffel over many years and I really
wonder why no other language (except maybe D) supports it.

Also note that as least as important as runtime verification is the
self-documentation aspect of code contracts. And for this documentation
aspect it is important for the contracts to be part of the method
signature and not the body.

Being part of the signature would be nice, but not technically necessary. Essentially you are just moving the contracts somewhere else. Perhaps something along these lines (just off the top of my head), a "where" block for pre-conditions and a "result" block for post-conditions, to be used immediately following:

def foo(arg1: Int, arg2: Int): Int
   where(arg1 >= arg2; arg1 != 0; this.someField > arg2;} // multiple contracts, in the form of (Unit => Boolean) delimited by semicolons, enclosing the parameters of foo and "this"
   result(returnValue => returnValue >= 0 && returnValue < arg2) = {... method body... }

Bytecode transformation is only a hack if you do not want to change the
language anymore - but since Scala is still evolving it might still be
possible to add it as a language feature...

True, but one could also argue that if a sufficiently good implementation can be made without a new language feature, then that implementation would be preferable. The implementation would be far easier as a "library plus late-phase compiler plugin" than "library plus new scala syntax".

Of course, you could always start with the compiler plugin method, then introduce a new language feature down the road that produces an equivalent to what is generated by the compiler plugin, if it proves to be desirable.
Jann Röder
Joined: 2010-07-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract

> I disagree that code contracts are not practical for a non-research
> language. I have used Code Contracts in my own projects, and while I
> found it took some non-trivial work introducing contracts to an existing
> code-base (and there were a few confusing warnings that were generally
> addressed by introducing Assumptions), once the contracts were in place
> and I was writing contracts for any new code, the overhead was
> negligible, especially considering the benefits.
>
> Also, scala's syntax could possibly allow for more succinct definition
> of contracts than is possible in C#.

That is good to hear. I concluded this from the paper I mentioned, I
never used Spec# myself. But I really doubt that Boogie can prove
complex contracts without a lot of annotation support. I suppose just
having no warnings doesn't mean that all contracts are proven to always
hold.

> Being part of the signature would be nice, but not technically
> necessary. Essentially you are just moving the contracts somewhere else.
> Perhaps something along these lines (just off the top of my head), a
> "where" block for pre-conditions and a "result" block for
> post-conditions, to be used immediately following:

I don't know what can be done with a compiler plugin but I think it is
very important that the contract syntax is very concise and feels like
it belongs to the language. I tried several DbC implementations for Java
but none of them seemed to work properly. The technologically most
convincing one was Modern Jass (http://modernjass.sourceforge.net/), but
I could not get it to work. It uses a compiler plugin and the contracts
are specified in annotations. Annotations have the big disadvantage that
the compiler does not check their content. At least in java this seems
to be the case. Therefore other methods are preferable. Adapting Spec#'
syntax to Scala would look something like this, which I think is quite OK.

def method(a: String): String
requires a.contains("k")
requires (condition2, "Some comment")
ensures !Result.isEmpty
= {
// Do something
}

Contracts also require the definition of at least two new language
keywords if the contracts should be type checked. Those are old()
to refer to a variable's value before the execution of a method and
Result (or similar) to refer to the return value.

Jann

David Pollak
Joined: 2008-12-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract


On Thu, Jul 8, 2010 at 12:17 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
On Thu, Jul 8, 2010 at 1:47 PM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
> Coming to Scala, I found that a lot of the stuff that I did with DbC >
could be done with the type system.  And when it's done with the type >
system, it's compile-time enforced and it's more obvious to the
> library consumer what the constraints are.

Unless I'm missing something the only "contract" you can enforce with
the type system is that an argument or return values is not null. You
are probably referring to the Option class here since Scala's
non-nullable types don't seem to be ready yet. The Eiffel compiler has
introduced void-safety about two years ago and there are still open
problems. For something like that to really work the entire base library
must support it - which is far from trivial (e.g. Arrays).

Of course I don't consider things like "the argument must be of type X"
a contract.

 I am also confused as to how scala's type system could be used as a replacement for generalized contracts (in other words, anything beyond simple "parameter is non-null" or "return value is non-null" type contracts). Maybe someone could give an example? I would be curious to see this.

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

object BiggerThanFour {
  implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
  implicit def take(in: BiggerThanFour): Int = in.value
}

def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
  i - j

def add(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
  (i: Int) + j

println(add(33, 44): Int)

println(subtract(44, 8): Int)

println(subtract(8, 44): Int)


 

 
> I highly suggest looking at the Code Contracts Microsoft research
> project:

After reading this quite interesting paper:
http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own&id=BarnettEA10.pdf
I think that the code contracts project is what the Spec# people could
rescue over into the production .NET framework. Spec# is dead now and
they did not want to really introduce contracts into C#. I also conclude
that static verification of code contracts will always be very limited
in "normal" programming languages. The spec# people had to introduce
lots of annotations to help the verifier. This is of course not
practical for a non-research language.

I disagree that code contracts are not practical for a non-research language. I have used Code Contracts in my own projects, and while I found it took some non-trivial work introducing contracts to an existing code-base (and there were a few confusing warnings that were generally addressed by introducing Assumptions), once the contracts were in place and I was writing contracts for any new code, the overhead was negligible, especially considering the benefits.

Also, scala's syntax could possibly allow for more succinct definition of contracts than is possible in C#.
 
On the other hand interface contracts with runtime verification have
proven to be useful and practical in Eiffel over many years and I really
wonder why no other language (except maybe D) supports it.

Also note that as least as important as runtime verification is the
self-documentation aspect of code contracts. And for this documentation
aspect it is important for the contracts to be part of the method
signature and not the body.

Being part of the signature would be nice, but not technically necessary. Essentially you are just moving the contracts somewhere else. Perhaps something along these lines (just off the top of my head), a "where" block for pre-conditions and a "result" block for post-conditions, to be used immediately following:

def foo(arg1: Int, arg2: Int): Int
   where(arg1 >= arg2; arg1 != 0; this.someField > arg2;} // multiple contracts, in the form of (Unit => Boolean) delimited by semicolons, enclosing the parameters of foo and "this"
   result(returnValue => returnValue >= 0 && returnValue < arg2) = {... method body... }

Bytecode transformation is only a hack if you do not want to change the
language anymore - but since Scala is still evolving it might still be
possible to add it as a language feature...

True, but one could also argue that if a sufficiently good implementation can be made without a new language feature, then that implementation would be preferable. The implementation would be far easier as a "library plus late-phase compiler plugin" than "library plus new scala syntax".

Of course, you could always start with the compiler plugin method, then introduce a new language feature down the road that produces an equivalent to what is generated by the compiler plugin, if it proves to be desirable.



--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics
James Iry
Joined: 2008-08-19,
User offline. Last seen 1 year 23 weeks ago.
Re: Re: Design By Contract
Using immutable types and phantom typing you can do all kinds of fun stuff. The following code statically ensures that I can't launch the rocket until I give it fuel and O2, but it doesn't matter what order, and I can't put fuel or O2 into a rocket that already has them.  That's a protocol and a contract.
sealed trait FuelStatetrait Fueled extends FuelStatetrait NoFuel extends FuelState
sealed trait O2Statetrait O2Ready extends O2State trait NoO2 extends O2State
sealed abstract class Rocket[F <: FuelState, O <: O2State](val payload : String)object Rocket {   def apply(payload : String) = new Rocket[NoFuel, NoO2](payload){}    def giveO2[F <: FuelState](r : Rocket[F, NoO2]) = new Rocket[F, O2Ready](r.payload){}   def giveFuel[O <: O2State](r : Rocket[NoFuel, O]) = new Rocket[Fueled, O](r.payload){}   def launch(r : Rocket[Fueled, O2Ready]) = "launched with a payload of " + r.payload + "!" }
scala> val r1 = Rocket("astronauts")r1: Rocket[NoFuel,NoO2] = Rocket$$anon$1@4d885088
scala> val r2 = Rocket.giveFuel(r1) r2: Rocket[Fueled,NoO2] = Rocket$$anon$3@3b274069
scala> val r3 = Rocket.giveO2(r2)r3: Rocket[Fueled,O2Ready] = Rocket$$anon$2@36c51089
scala> val result = Rocket.launch(r3) result: java.lang.String = launched with a payload of astronauts!
scala> Rocket.giveFuel(r2)<console>:16: error: type mismatch; found   : Rocket[Fueled,NoO2]  required: Rocket[NoFuel,?]       Rocket.giveFuel(r2)                       ^
scala> Rocket.launch(r1)<console>:15: error: type mismatch; found   : Rocket[NoFuel,NoO2]  required: Rocket[Fueled,O2Ready]       Rocket.launch(r1)


On Thu, Jul 8, 2010 at 10:47 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:


Unless I'm missing something the only "contract" you can enforce with
the type system is that an argument or return values is not null. You
are probably referring to the Option class here since Scala's
non-nullable types don't seem to be ready yet. The Eiffel compiler has
introduced void-safety about two years ago and there are still open
problems. For something like that to really work the entire base library
must support it - which is far from trivial (e.g. Arrays).

Of course I don't consider things like "the argument must be of type X"
a contract.

> I highly suggest looking at the Code Contracts Microsoft research
> project:

After reading this quite interesting paper:
http://people.inf.ethz.ch/lehnerh/pm/publications/getpdf.php?bibname=Own&id=BarnettEA10.pdf
I think that the code contracts project is what the Spec# people could
rescue over into the production .NET framework. Spec# is dead now and
they did not want to really introduce contracts into C#. I also conclude
that static verification of code contracts will always be very limited
in "normal" programming languages. The spec# people had to introduce
lots of annotations to help the verifier. This is of course not
practical for a non-research language.

On the other hand interface contracts with runtime verification have
proven to be useful and practical in Eiffel over many years and I really
wonder why no other language (except maybe D) supports it.

Also note that as least as important as runtime verification is the
self-documentation aspect of code contracts. And for this documentation
aspect it is important for the contracts to be part of the method
signature and not the body.

Bytecode transformation is only a hack if you do not want to change the
language anymore - but since Scala is still evolving it might still be
possible to add it as a language feature...

Jann


nilskp
Joined: 2009-01-30,
User offline. Last seen 1 year 27 weeks ago.
Re: Re: Design By Contract
On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.
Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract


On Thu, Jul 8, 2010 at 8:27 PM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:
On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.

also, there is no way to globally enable/disable contracts using this method, or to easily add/change contracts, unless I'm missing something?
dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Design By Contract
scalac -Xdisable-assertions

On Thu, Jul 8, 2010 at 11:16 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:


On Thu, Jul 8, 2010 at 8:27 PM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:
On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.

also, there is no way to globally enable/disable contracts using this method, or to easily add/change contracts, unless I'm missing something?



--
Daniel C. Sobral

I travel to the future all the time.
Will Sargent
Joined: 2010-06-05,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract


On Thu, Jul 8, 2010 at 8:57 AM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:
Jann,
I was a fan of DbC until I started using Scala.  One of the things that drove me out of the Ruby community was the absolute unwillingness to add DbC concepts to the language (my thought was that if optional static typing was not on the table, at least support DbC at the language level [there was a library for DbC but the syntax was not inviting.])

Coming to Scala, I found that a lot of the stuff that I did with DbC could be done with the type system.  And when it's done with the type system, it's compile-time enforced and it's more obvious to the library consumer what the constraints are.

My 2 cents.

That's funny -- I've had the exact same thought about DbC and Ruby.  In my mind, anything that narrows the amount of run time testing you have to do is a good thing, especially if you can limit your possible begin and end states and have them checked and enforced by the system itself.

The coolest software engineering trick I've ever seen is ESC/Java2: a static analysis tool that could look at the pre and post conditions in Java, defined in JML, then look at the structure of the code in memory, and then tell you if the code met the conditions.  At compile time.

Here's my blog post about it: http://tersesystems.com/post/3300057.jhtml

It's been a while since I looked at it, but it's a beautiful system. 

I think static analysis is going to be the next wave of software engineering, once computing power increases to the point where cores are cheap and IDEs can attempt to follow your logic as you write your code.  I don't think it will ever replace integration or system testing just because the possible set of states is so large, but I can easily see an IDE automatically generating pre/post conditions for your code as you write it, and then telling you as soon as you've written code that breaks those conditions.

Will.

Danielk
Joined: 2009-06-08,
User offline. Last seen 3 years 21 weeks ago.
Re: Re: Design By Contract
Note though that Design by Contract is a runtime thing. Sure, it is even better if some conditions can be verifed statically, but that will never get as far as the assertions possible at runtime. Taking BiggerThanFour as an example, this is a trivial check at runtime. Trying to verify it statically though would be a research project, and for many cases it wouldn't be possible to determine whether the contract is fulfilled or not.

On Fri, Jul 9, 2010 at 2:27 AM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:
On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.

Luc Duponcheel
Joined: 2008-12-19,
User offline. Last seen 34 weeks 3 days ago.
Re: Re: Design By Contract

on the other hand, as Edsger W. Dijkstra quoted many years ago

> Program testing can be used to show the presence of bugs, but never to show their absence!

translated to compile-time versus runtime Design by Contract

o compile time verification can give you some degree of confidence
that code is correct
o runtime verification can only give you full evidence that code is not correct

Luc

On Fri, Jul 9, 2010 at 10:25 AM, Daniel Kristensen
wrote:
> Note though that Design by Contract is a runtime thing. Sure, it is even
> better if some conditions can be verifed statically, but that will never get
> as far as the assertions possible at runtime. Taking BiggerThanFour as an
> example, this is a trivial check at runtime. Trying to verify it statically
> though would be a research project, and for many cases it wouldn't be
> possible to determine whether the contract is fulfilled or not.
>
> On Fri, Jul 9, 2010 at 2:27 AM, Nils Kilden-Pedersen
> wrote:
>>
>> On Thu, Jul 8, 2010 at 4:05 PM, David Pollak
>> wrote:
>>>
>>> final case class BiggerThanFour(value: Int) {
>>>   assert(value > 4)
>>> }
>>
>> That just saves you the runtime check in multiple places. Using assert
>> (must use -ea to work) or better yet require would still cause a runtime
>> exception, not a compiler error/warning.
>
>

Stefan Langer
Joined: 2009-10-23,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract

And how would you ensure a static check in this context.

At least the tyope BiggerThanFour guarantees that if the runtime check
succeeds anywhere where BiggerThanFour is used it is guaranteed that
it is bigger then four. Which in my eyes is a perfect contract
enforcement.
So if you encode the contract into types you can rest assured that as
long as the contract works in those types the contract is enforced in
all places the type is used.

-Stefan

2010/7/9 Nils Kilden-Pedersen :
> On Thu, Jul 8, 2010 at 4:05 PM, David Pollak
> wrote:
>>
>> final case class BiggerThanFour(value: Int) {
>>   assert(value > 4)
>> }
>
> That just saves you the runtime check in multiple places. Using assert (must
> use -ea to work) or better yet require would still cause a runtime
> exception, not a compiler error/warning.
>

Grand, Mark D.
Joined: 2009-12-24,
User offline. Last seen 42 years 45 weeks ago.
RE: Re: Design By Contract

Runtime assertions tell you about assertions that were actually violated during testing.  Static analysis and symbolic execution tell you about assertions that could be violated even though you did not take time to write code to exercise those cases.  It has the potential to be a BIG time saver.

 

From: Daniel Kristensen [mailto:daniel [dot] kristensen [at] gmail [dot] com]
Sent: Friday, July 09, 2010 4:26 AM
To: Nils Kilden-Pedersen
Cc: David Pollak; Jeremy Bell; Jann Röder; scala [at] listes [dot] epfl [dot] ch
Subject: Re: [scala] Re: Design By Contract

 

Note though that Design by Contract is a runtime thing. Sure, it is even better if some conditions can be verifed statically, but that will never get as far as the assertions possible at runtime. Taking BiggerThanFour as an example, this is a trivial check at runtime. Trying to verify it statically though would be a research project, and for many cases it wouldn't be possible to determine whether the contract is fulfilled or not.

On Fri, Jul 9, 2010 at 2:27 AM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:

On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

 

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

 

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.

 


This e-mail message (including any attachments) is for the sole use of
the intended recipient(s) and may contain confidential and privileged
information. If the reader of this message is not the intended
recipient, you are hereby notified that any dissemination, distribution
or copying of this message (including any attachments) is strictly
prohibited.

If you have received this message in error, please contact
the sender by reply e-mail message and destroy all copies of the
original message (including attachments).
Danielk
Joined: 2009-06-08,
User offline. Last seen 3 years 21 weeks ago.
Re: Re: Design By Contract
I don't need convincing - I think good static analysis is extremely valuable. But when it isn't feasible to check something statically, I think runtime checks are a lot better than nothing. Especially when they're nicely factored into a type with a name clearly expressing the contract as in the BiggerThanFour example.

Also, I interpreted the OP's question to be about Design by Contract - not necessarily static analysis. So I think David's example with BiggerThanFour was poerfectly relevant.

Cheers,
Daniel


On Fri, Jul 9, 2010 at 1:09 PM, Grand, Mark D <mgrand [at] emory [dot] edu> wrote:

Runtime assertions tell you about assertions that were actually violated during testing.  Static analysis and symbolic execution tell you about assertions that could be violated even though you did not take time to write code to exercise those cases.  It has the potential to be a BIG time saver.

 

From: Daniel Kristensen [mailto:daniel [dot] kristensen [at] gmail [dot] com]
Sent: Friday, July 09, 2010 4:26 AM
To: Nils Kilden-Pedersen
Cc: David Pollak; Jeremy Bell; Jann Röder; scala [at] listes [dot] epfl [dot] ch
Subject: Re: [scala] Re: Design By Contract

 

Note though that Design by Contract is a runtime thing. Sure, it is even better if some conditions can be verifed statically, but that will never get as far as the assertions possible at runtime. Taking BiggerThanFour as an example, this is a trivial check at runtime. Trying to verify it statically though would be a research project, and for many cases it wouldn't be possible to determine whether the contract is fulfilled or not.

On Fri, Jul 9, 2010 at 2:27 AM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:

On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com> wrote:

 

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

 

That just saves you the runtime check in multiple places. Using assert (must use -ea to work) or better yet require would still cause a runtime exception, not a compiler error/warning.

 


This e-mail message (including any attachments) is for the sole use of
the intended recipient(s) and may contain confidential and privileged
information. If the reader of this message is not the intended
recipient, you are hereby notified that any dissemination, distribution
or copying of this message (including any attachments) is strictly
prohibited.

If you have received this message in error, please contact
the sender by reply e-mail message and destroy all copies of the
original message (including attachments).

nilskp
Joined: 2009-01-30,
User offline. Last seen 1 year 27 weeks ago.
Re: Re: Re: Design By Contract
On Fri, Jul 9, 2010 at 5:25 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
And how would you ensure a static check in this context.

I wouldn't. My comment was only that adding types is not a substitute for DbC, it merely changes how the runtime validation is achieved. It doesn't add any further safety. And I would regard it as incorrect to use assert for any DbC because it can be disabled (in fact is disabled by default).
 

At least the tyope BiggerThanFour guarantees that if the runtime check
succeeds anywhere where BiggerThanFour is used it is guaranteed that
it is bigger then four. Which in my eyes is a perfect contract
enforcement.
So if you encode the contract into types you can rest assured that as
long as the contract works in those types the contract is enforced in
all places the type is used.

-Stefan

2010/7/9 Nils Kilden-Pedersen <nilskp [at] gmail [dot] com>:
> On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com>
> wrote:
>>
>> final case class BiggerThanFour(value: Int) {
>>   assert(value > 4)
>> }
>
> That just saves you the runtime check in multiple places. Using assert (must
> use -ea to work) or better yet require would still cause a runtime
> exception, not a compiler error/warning.
>

David Pollak
Joined: 2008-12-16,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Re: Design By Contract
Folks,

First, the BiggerThanFour example was a trivial example that I threw together in 5 minutes.  It's not meant to be much more than using an explicit type to achieve a two-fold goal: (1) encode some approximation of the contract (yeah, maybe I should have used assert, blah blah) and (2) (this is the important one) flag to the developer in ScalaDocs what the contract is.  The latter in my mind is a lot more important.

By being able to flag to the developer what the constraint is (rather than having the developer real more than 5 words of the documentation for the method), the developer is more likely to get it right.

James showed an excellent example.  Here's another (less excellent example from Lift):

    User.find(By(User.email, "foo [at] bar [dot] com")) // legal
    User.find(By(User.birthday, new Date("Jan 4, 1975"))) // legal
    User.find(By(User.birthday, "foo [at] bar [dot] com")) // compiler error

In both Ruby and Java, there's very little compile-time checking of parameter types for query building (in Ruby there's none).  In Scala it was easy to encode a compile-time check of Date field to Date parameter and String field to String parameter.  It's possible in Java, but I have not seen it in done.

So, I stand by my original assertion: "I found that a lot of the stuff that I did with DbC could be done with the type system."  I did not claim a 100% of what a complete DbC system can do can be done with Scala's type system.  But at the end of the day, in Java and in Ruby, lots of stuff is just Strings or Objects and you really need DbC to make sure that the Strings/hash/Objects are what you expect them to be.

Further, with Option, many (not all) of the null problems go away.  Why?  (1) the library authors flag a method as not having a computable result (2) library consumers are faced with something that really might not contain a value (unless they are idiots like me who did an implicit conversion from Option[T] to T) (3) (this is the important one) developers get into the groove of not using null.

More broadly, I try to solve for common problems rather than the universe of problems.  Scala's type system allows me to solve for common errors.  Even if it don't banish null or do everything that Ada does, Scala's type system gives me many of the tools I need to write non-DbC code that's low in bugs.

Thanks,

David

On Fri, Jul 9, 2010 at 4:55 AM, Nils Kilden-Pedersen <nilskp [at] gmail [dot] com> wrote:
On Fri, Jul 9, 2010 at 5:25 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
And how would you ensure a static check in this context.

I wouldn't. My comment was only that adding types is not a substitute for DbC, it merely changes how the runtime validation is achieved. It doesn't add any further safety. And I would regard it as incorrect to use assert for any DbC because it can be disabled (in fact is disabled by default).
 

At least the tyope BiggerThanFour guarantees that if the runtime check
succeeds anywhere where BiggerThanFour is used it is guaranteed that
it is bigger then four. Which in my eyes is a perfect contract
enforcement.
So if you encode the contract into types you can rest assured that as
long as the contract works in those types the contract is enforced in
all places the type is used.

-Stefan

2010/7/9 Nils Kilden-Pedersen <nilskp [at] gmail [dot] com>:
> On Thu, Jul 8, 2010 at 4:05 PM, David Pollak <feeder [dot] of [dot] the [dot] bears [at] gmail [dot] com>
> wrote:
>>
>> final case class BiggerThanFour(value: Int) {
>>   assert(value > 4)
>> }
>
> That just saves you the runtime check in multiple places. Using assert (must
> use -ea to work) or better yet require would still cause a runtime
> exception, not a compiler error/warning.
>




--
Lift, the simply functional web framework http://liftweb.net
Beginning Scala http://www.apress.com/book/view/1430219890
Follow me: http://twitter.com/dpp
Blog: http://goodstuff.im
Surf the harmonics
Jann Röder
Joined: 2010-07-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Design By Contract

So to summarize:
* Quite a few people are convinced of the benefits of Design by
Contract, for both runtime checking and the possibility to do extended
static checking. I would also add the self documentation aspect.

* Even though you can do some funny things with Scala's type system and
implicit conversions, this is not what design by contract is about - in
my opinion. I really don't want to create a special type to put a
contract on a method argument.

* Even though a library + compiler plugin approach is preferred over a
language extension, I'm not convinced that full-blown DbC support can be
achieved without modifying the language.

Conclusion: It needs to be determined if there is a large enough general
interest for adding DbC to the language. Also it needs to be seen if the
Scala core team and Dr. Odersky are not opposed to this feature.

Jann

geoff
Joined: 2008-08-20,
User offline. Last seen 1 year 25 weeks ago.
Re: Re: Design By Contract

On Fri, Jul 09, 2010 at 05:34:18PM +0200, Jann Röder said
> * Even though a library + compiler plugin approach is preferred over a
> language extension, I'm not convinced that full-blown DbC support can be
> achieved without modifying the language.

About a year ago I did some work in this direction hoping to have
something to show for the scala lift off. I didn't get something working
for that, but it was enough to see a path forward for a compiler plugin.
I believe that the core scala team is interested in broadening the
possiblilities for compiler plugins, so if there is a rather large
hurdle I think there'd be a strong possibility of tweaking the compiler
interfaces to make it easier.

I'm still interested in working on a DbC plugin for scala, but my spare
coding cycles are currently occupied by an LLVM target for the
compiler.[1]

havelund
Joined: 2009-12-31,
User offline. Last seen 29 weeks 4 days ago.
Re: Re: Design By Contract

Concerning contracts in Scala, I would like to refer your attention to the invited talk:

  "Contracts in Scala"
 
to be presented at RV 2010 (Runtime Verification, November 1-4, 2010):

  http://rv2010.org

by Martin Odersky, see specifically:

  http://rv2010.org/invited.php

As co-chair of this event I encourage you to attend the conference.

Klaus Havelund


On Fri, Jul 9, 2010 at 8:34 AM, Jann Röder <roederja [at] ethz [dot] ch> wrote:
So to summarize:
* Quite a few people are convinced of the benefits of Design by
Contract, for both runtime checking and the possibility to do extended
static checking. I would also add the self documentation aspect.

* Even though you can do some funny things with Scala's type system and
implicit conversions, this is not what design by contract is about - in
my opinion. I really don't want to create a special type to put a
contract on a method argument.

* Even though a library + compiler plugin approach is preferred over a
language extension, I'm not convinced that full-blown DbC support can be
achieved without modifying the language.

Conclusion: It needs to be determined if there is a large enough general
interest for adding DbC to the language. Also it needs to be seen if the
Scala core team and Dr. Odersky are not opposed to this feature.

Jann


Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract


On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen <daniel [dot] kristensen [at] gmail [dot] com> wrote:
I don't need convincing - I think good static analysis is extremely valuable. But when it isn't feasible to check something statically, I think runtime checks are a lot better than nothing. Especially when they're nicely factored into a type with a name clearly expressing the contract as in the BiggerThanFour example.

Also, I interpreted the OP's question to be about Design by Contract - not necessarily static analysis. So I think David's example with BiggerThanFour was poerfectly relevant.

Cheers,
Daniel


I'm not completely convinced of the benefits of wrapper types for enforcing design contracts over simply implementing the contracts similarly to other frameworks, for the following reasons:

  • First of all, you have to introduce a new type for each contract, or even multiple types that get mixed in for multiple contracts. This obfuscates your interface for the person that has to use your method. I have to track down every implicit conversion for every parameter of your function just to figure out what I'm supposed to send to it.
  • Wrapper classes with implicit conversions are slow, and using this method it is far more difficult to write a plugin that removes the contract checks in release mode. You can remove the asserts, but the implicit conversion remains. This discourages the use of contracts.
  • You can't write contracts which involve more than one parameter.
  • Adding new contracts or removing contracts becomes difficult - you have to change your wrapper type, or mixin multiple contract wrappers. 
  • There is more typing overhead involved. Why is it more elegant to have a wrapper class than to just have the tooling extract the pre and post-conditions from the begging of the method and show them to you in the editor and the documentation?

To demonstrate my point, compare the Code Contracts style to the Wrapper Type Contract style in the BiggerThanFour exmaple. Here is the original BiggerThanFour example:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

object BiggerThanFour {
  implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
  implicit def take(in: BiggerThanFour): Int = in.value
}

def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
  i - j

Here is what it would look like if we just implemented Code Contracts in scala (without adding new syntax):

def subtract(i: Int, j: Int): Int = {
   Requires(i > 4 && j > 4)
   Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the real return value for Result[Int]()
   i - j
}

Or, using jaan's suggestion involving new syntax:
def subtract(i: Int, j: Int): Int
    Requires(i > 4 && j > 4)
    Ensures(Result > 4) // assuming the compiler makes Result an Int here implicitly
   = i - j

To me, both of these look more succinct, elegant, and flexible than the BiggerThanFour approach.


Also, regarding static analysis: In my experience with Code Contracts, I've found some situations where the analyzer can't prove a contract has not been violated, however the analyzer can tell when it can't prove a contract, and will issue a warning to this effect. I found that this happened less often than I thought it would. In a project of around 15,000 lines of code, I think this happened only three times. To be fair - the project didn't dynamically load assemblies or use the dynamic language runtime or any similar situation where there is more information available at runtime than at compile time.

If this happens, usually there is an obvious reason that you can address easily. Otherwise, as a last resort you can insert Assume calls into the code to give the analyzer the information it needs to prove a contract hasn't been violated. Assume calls are also evaluated and checked at run-time to ensure that your assumptions are indeed correct.
dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Design By Contract
This is already valid Scala:
def subtract(i: Int, j: Int): Int = {
   require(i > 4 && j > 4)
   (i - j).ensuring(_ > 4)
}

On Fri, Jul 9, 2010 at 1:23 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:


On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen <daniel [dot] kristensen [at] gmail [dot] com> wrote:
I don't need convincing - I think good static analysis is extremely valuable. But when it isn't feasible to check something statically, I think runtime checks are a lot better than nothing. Especially when they're nicely factored into a type with a name clearly expressing the contract as in the BiggerThanFour example.

Also, I interpreted the OP's question to be about Design by Contract - not necessarily static analysis. So I think David's example with BiggerThanFour was poerfectly relevant.

Cheers,
Daniel


I'm not completely convinced of the benefits of wrapper types for enforcing design contracts over simply implementing the contracts similarly to other frameworks, for the following reasons:

  • First of all, you have to introduce a new type for each contract, or even multiple types that get mixed in for multiple contracts. This obfuscates your interface for the person that has to use your method. I have to track down every implicit conversion for every parameter of your function just to figure out what I'm supposed to send to it.
  • Wrapper classes with implicit conversions are slow, and using this method it is far more difficult to write a plugin that removes the contract checks in release mode. You can remove the asserts, but the implicit conversion remains. This discourages the use of contracts.
  • You can't write contracts which involve more than one parameter.
  • Adding new contracts or removing contracts becomes difficult - you have to change your wrapper type, or mixin multiple contract wrappers. 
  • There is more typing overhead involved. Why is it more elegant to have a wrapper class than to just have the tooling extract the pre and post-conditions from the begging of the method and show them to you in the editor and the documentation?

To demonstrate my point, compare the Code Contracts style to the Wrapper Type Contract style in the BiggerThanFour exmaple. Here is the original BiggerThanFour example:

final case class BiggerThanFour(value: Int) {
  assert(value > 4)
}

object BiggerThanFour {
  implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
  implicit def take(in: BiggerThanFour): Int = in.value
}

def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
  i - j

Here is what it would look like if we just implemented Code Contracts in scala (without adding new syntax):

def subtract(i: Int, j: Int): Int = {
   Requires(i > 4 && j > 4)
   Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the real return value for Result[Int]()
   i - j
}

Or, using jaan's suggestion involving new syntax:
def subtract(i: Int, j: Int): Int
    Requires(i > 4 && j > 4)
    Ensures(Result > 4) // assuming the compiler makes Result an Int here implicitly
   = i - j

To me, both of these look more succinct, elegant, and flexible than the BiggerThanFour approach.


Also, regarding static analysis: In my experience with Code Contracts, I've found some situations where the analyzer can't prove a contract has not been violated, however the analyzer can tell when it can't prove a contract, and will issue a warning to this effect. I found that this happened less often than I thought it would. In a project of around 15,000 lines of code, I think this happened only three times. To be fair - the project didn't dynamically load assemblies or use the dynamic language runtime or any similar situation where there is more information available at runtime than at compile time.

If this happens, usually there is an obvious reason that you can address easily. Otherwise, as a last resort you can insert Assume calls into the code to give the analyzer the information it needs to prove a contract hasn't been violated. Assume calls are also evaluated and checked at run-time to ensure that your assumptions are indeed correct.



--
Daniel C. Sobral

I travel to the future all the time.
Stefan Langer
Joined: 2009-10-23,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract

I disagree I think a contract is the essence of an interface. Every
interface has a signature which states which types it accepts and it
has certain rules governing its usage. Some of these rules can be
expressed through the type system and others have to be checked by the
implementer but still it is assumed that they are not violated.

Examples:
Monads have laws governing them if they are not fullfilled you do not
have a Monad. These laws can not be guaranteed by the signature but
have to be assured by the implementation (please correct me if this is
false)
Ordered has the assumption that the elements have a stable order. This
is part of the contract. It is expressed by the usage of the Ordered
Trait that you are fullfilling the contract but still the compiler
cannot guarantee that the compare method is correctly implemented.
e.g
class WeirdOrderedInteger(val i: Int) extends Ordered[Int] {
def compare(i1: Int, i2: Int): Int = {
val r = Random.nextInt(40)
if (r == i) 0 else if(r > 20) -1 else 1
}
}

I think this applies to any DbC as well. So a wrapper type is just a
way of making the contract more explicit and enabling the compiler to
catch violations early on.
Changing the contract therefor is on the same level as changing a
signature or a class it is a change in the underlying interface and
the way the whole system behaves.

-Stefan

2010/7/9 Jeremy Bell :
>
>
> On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen
> wrote:
>>
>> I don't need convincing - I think good static analysis is extremely
>> valuable. But when it isn't feasible to check something statically, I think
>> runtime checks are a lot better than nothing. Especially when they're nicely
>> factored into a type with a name clearly expressing the contract as in the
>> BiggerThanFour example.
>>
>> Also, I interpreted the OP's question to be about Design by Contract - not
>> necessarily static analysis. So I think David's example with BiggerThanFour
>> was poerfectly relevant.
>>
>> Cheers,
>> Daniel
>
>
> I'm not completely convinced of the benefits of wrapper types for enforcing
> design contracts over simply implementing the contracts similarly to other
> frameworks, for the following reasons:
>
> First of all, you have to introduce a new type for each contract, or even
> multiple types that get mixed in for multiple contracts. This obfuscates
> your interface for the person that has to use your method. I have to track
> down every implicit conversion for every parameter of your function just to
> figure out what I'm supposed to send to it.
> Wrapper classes with implicit conversions are slow, and using this method it
> is far more difficult to write a plugin that removes the contract checks in
> release mode. You can remove the asserts, but the implicit conversion
> remains. This discourages the use of contracts.
> You can't write contracts which involve more than one parameter.
> Adding new contracts or removing contracts becomes difficult - you have to
> change your wrapper type, or mixin multiple contract wrappers.
> There is more typing overhead involved. Why is it more elegant to have a
> wrapper class than to just have the tooling extract the pre and
> post-conditions from the begging of the method and show them to you in the
> editor and the documentation?
>
> To demonstrate my point, compare the Code Contracts style to the Wrapper
> Type Contract style in the BiggerThanFour exmaple. Here is the original
> BiggerThanFour example:
>
> final case class BiggerThanFour(value: Int) {
>   assert(value > 4)
> }
>
> object BiggerThanFour {
>   implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
>   implicit def take(in: BiggerThanFour): Int = in.value
> }
>
> def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
>   i - j
>
> Here is what it would look like if we just implemented Code Contracts in
> scala (without adding new syntax):
>
> def subtract(i: Int, j: Int): Int = {
>    Requires(i > 4 && j > 4)
>    Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the
> real return value for Result[Int]()
>    i - j
> }
>
> Or, using jaan's suggestion involving new syntax:
> def subtract(i: Int, j: Int): Int
>     Requires(i > 4 && j > 4)
>     Ensures(Result > 4) // assuming the compiler makes Result an Int here
> implicitly
>    = i - j
>
> To me, both of these look more succinct, elegant, and flexible than the
> BiggerThanFour approach.
>
>
> Also, regarding static analysis: In my experience with Code Contracts, I've
> found some situations where the analyzer can't prove a contract has not been
> violated, however the analyzer can tell when it can't prove a contract, and
> will issue a warning to this effect. I found that this happened less often
> than I thought it would. In a project of around 15,000 lines of code, I
> think this happened only three times. To be fair - the project didn't
> dynamically load assemblies or use the dynamic language runtime or any
> similar situation where there is more information available at runtime than
> at compile time.
>
> If this happens, usually there is an obvious reason that you can address
> easily. Otherwise, as a last resort you can insert Assume calls into the
> code to give the analyzer the information it needs to prove a contract
> hasn't been violated. Assume calls are also evaluated and checked at
> run-time to ensure that your assumptions are indeed correct.
>

Jeremy Bell
Joined: 2010-04-08,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract
Perhaps I should clarify. I don't disagree with the idea that contracts should be part of the "interface". What I was trying to say was that the wrapper class method of implementing contracts as interface has some limitations and drawbacks, among them the fact that they do not actually ensure the contract is fulfilled at compile time.

However, I'm also not saying that a static verifier is the only solution either. The main goal of contracts as interface is to prevent incorrect usage at compile time, and there is more than one path to this goal.

For example, this can be achieved through scala's type system, if you accept certain limitations.  The rocket ship example works quite elegantly, but (correct me if I'm wrong) it relies on the fact that the RocketShip class is immutable.

The static verifier/plugin route is also not without its flaws, but I think it strikes a good practical balance for the general case, when a more elegant solution can't be used.

Regards,
Jeremy Bell


On Mon, Jul 12, 2010 at 4:29 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
I disagree I think a contract is the essence of an interface. Every
interface has a signature which states which types it accepts and it
has certain rules governing its usage. Some of these rules can be
expressed through the type system and others have to be checked by the
implementer but still it is assumed that they are not violated.

Examples:
Monads have laws governing them if they are not fullfilled you do not
have a Monad. These laws can not be guaranteed by the signature but
have to be assured by the implementation (please correct me if this is
false)
Ordered has the assumption that the elements have a stable order. This
is part of the contract. It is expressed by the usage of the Ordered
Trait that you are fullfilling the contract but still the compiler
cannot guarantee that the compare method is correctly implemented.
e.g
class WeirdOrderedInteger(val i: Int) extends Ordered[Int] {
 def compare(i1: Int, i2: Int): Int = {
   val r = Random.nextInt(40)
   if (r == i) 0 else if(r > 20) -1 else 1
 }
}

I think this applies to any DbC as well. So a wrapper type is just a
way of making the contract more explicit and enabling the compiler to
catch violations early on.
Changing the contract therefor is on the same level as changing a
signature or a class it is a change in the underlying interface and
the way the whole system behaves.

-Stefan


2010/7/9 Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com>:
>
>
> On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen
> <daniel [dot] kristensen [at] gmail [dot] com> wrote:
>>
>> I don't need convincing - I think good static analysis is extremely
>> valuable. But when it isn't feasible to check something statically, I think
>> runtime checks are a lot better than nothing. Especially when they're nicely
>> factored into a type with a name clearly expressing the contract as in the
>> BiggerThanFour example.
>>
>> Also, I interpreted the OP's question to be about Design by Contract - not
>> necessarily static analysis. So I think David's example with BiggerThanFour
>> was poerfectly relevant.
>>
>> Cheers,
>> Daniel
>
>
> I'm not completely convinced of the benefits of wrapper types for enforcing
> design contracts over simply implementing the contracts similarly to other
> frameworks, for the following reasons:
>
> First of all, you have to introduce a new type for each contract, or even
> multiple types that get mixed in for multiple contracts. This obfuscates
> your interface for the person that has to use your method. I have to track
> down every implicit conversion for every parameter of your function just to
> figure out what I'm supposed to send to it.
> Wrapper classes with implicit conversions are slow, and using this method it
> is far more difficult to write a plugin that removes the contract checks in
> release mode. You can remove the asserts, but the implicit conversion
> remains. This discourages the use of contracts.
> You can't write contracts which involve more than one parameter.
> Adding new contracts or removing contracts becomes difficult - you have to
> change your wrapper type, or mixin multiple contract wrappers.
> There is more typing overhead involved. Why is it more elegant to have a
> wrapper class than to just have the tooling extract the pre and
> post-conditions from the begging of the method and show them to you in the
> editor and the documentation?
>
> To demonstrate my point, compare the Code Contracts style to the Wrapper
> Type Contract style in the BiggerThanFour exmaple. Here is the original
> BiggerThanFour example:
>
> final case class BiggerThanFour(value: Int) {
>   assert(value > 4)
> }
>
> object BiggerThanFour {
>   implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
>   implicit def take(in: BiggerThanFour): Int = in.value
> }
>
> def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
>   i - j
>
> Here is what it would look like if we just implemented Code Contracts in
> scala (without adding new syntax):
>
> def subtract(i: Int, j: Int): Int = {
>    Requires(i > 4 && j > 4)
>    Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the
> real return value for Result[Int]()
>    i - j
> }
>
> Or, using jaan's suggestion involving new syntax:
> def subtract(i: Int, j: Int): Int
>     Requires(i > 4 && j > 4)
>     Ensures(Result > 4) // assuming the compiler makes Result an Int here
> implicitly
>    = i - j
>
> To me, both of these look more succinct, elegant, and flexible than the
> BiggerThanFour approach.
>
>
> Also, regarding static analysis: In my experience with Code Contracts, I've
> found some situations where the analyzer can't prove a contract has not been
> violated, however the analyzer can tell when it can't prove a contract, and
> will issue a warning to this effect. I found that this happened less often
> than I thought it would. In a project of around 15,000 lines of code, I
> think this happened only three times. To be fair - the project didn't
> dynamically load assemblies or use the dynamic language runtime or any
> similar situation where there is more information available at runtime than
> at compile time.
>
> If this happens, usually there is an obvious reason that you can address
> easily. Otherwise, as a last resort you can insert Assume calls into the
> code to give the analyzer the information it needs to prove a contract
> hasn't been violated. Assume calls are also evaluated and checked at
> run-time to ensure that your assumptions are indeed correct.
>

adriaanm
Joined: 2010-02-08,
User offline. Last seen 31 weeks 4 days ago.
Re: Re: Design By Contract
From the academic point of view: types and contracts are not that different. Similarly, it would be nice to have a "dial" that determines the intensity of the type checker, which would go from JavaScript to Coq -- all in the same language. Regarding the first point: http://software.imdea.org/~aleks/papers/hoarelogic/jfpsep07.pdf
After reading that, imagine multiplying the expressivity of such a type system by the flexibility of the second point, the orthogonal feature of making a type system "gradual" (or "optional" or "pluggable" -- see ). This should address the concerns that contract-like types become unwieldy, whereas the polymorphism of the type system will ensure that contracts can be reused using standard language features (instead of repeating the mistake of adding something to the language as a second class citizen, and then reinventing polymorphism for it all over again).
adriaan
ps: follow ups welcome, but we should probably grab a beer and move to the debate room

On Mon, Jul 12, 2010 at 4:27 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
Perhaps I should clarify. I don't disagree with the idea that contracts should be part of the "interface". What I was trying to say was that the wrapper class method of implementing contracts as interface has some limitations and drawbacks, among them the fact that they do not actually ensure the contract is fulfilled at compile time.

However, I'm also not saying that a static verifier is the only solution either. The main goal of contracts as interface is to prevent incorrect usage at compile time, and there is more than one path to this goal.

For example, this can be achieved through scala's type system, if you accept certain limitations.  The rocket ship example works quite elegantly, but (correct me if I'm wrong) it relies on the fact that the RocketShip class is immutable.

The static verifier/plugin route is also not without its flaws, but I think it strikes a good practical balance for the general case, when a more elegant solution can't be used.

Regards,
Jeremy Bell


On Mon, Jul 12, 2010 at 4:29 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
I disagree I think a contract is the essence of an interface. Every
interface has a signature which states which types it accepts and it
has certain rules governing its usage. Some of these rules can be
expressed through the type system and others have to be checked by the
implementer but still it is assumed that they are not violated.

Examples:
Monads have laws governing them if they are not fullfilled you do not
have a Monad. These laws can not be guaranteed by the signature but
have to be assured by the implementation (please correct me if this is
false)
Ordered has the assumption that the elements have a stable order. This
is part of the contract. It is expressed by the usage of the Ordered
Trait that you are fullfilling the contract but still the compiler
cannot guarantee that the compare method is correctly implemented.
e.g
class WeirdOrderedInteger(val i: Int) extends Ordered[Int] {
 def compare(i1: Int, i2: Int): Int = {
   val r = Random.nextInt(40)
   if (r == i) 0 else if(r > 20) -1 else 1
 }
}

I think this applies to any DbC as well. So a wrapper type is just a
way of making the contract more explicit and enabling the compiler to
catch violations early on.
Changing the contract therefor is on the same level as changing a
signature or a class it is a change in the underlying interface and
the way the whole system behaves.

-Stefan


2010/7/9 Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com>:
>
>
> On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen
> <daniel [dot] kristensen [at] gmail [dot] com> wrote:
>>
>> I don't need convincing - I think good static analysis is extremely
>> valuable. But when it isn't feasible to check something statically, I think
>> runtime checks are a lot better than nothing. Especially when they're nicely
>> factored into a type with a name clearly expressing the contract as in the
>> BiggerThanFour example.
>>
>> Also, I interpreted the OP's question to be about Design by Contract - not
>> necessarily static analysis. So I think David's example with BiggerThanFour
>> was poerfectly relevant.
>>
>> Cheers,
>> Daniel
>
>
> I'm not completely convinced of the benefits of wrapper types for enforcing
> design contracts over simply implementing the contracts similarly to other
> frameworks, for the following reasons:
>
> First of all, you have to introduce a new type for each contract, or even
> multiple types that get mixed in for multiple contracts. This obfuscates
> your interface for the person that has to use your method. I have to track
> down every implicit conversion for every parameter of your function just to
> figure out what I'm supposed to send to it.
> Wrapper classes with implicit conversions are slow, and using this method it
> is far more difficult to write a plugin that removes the contract checks in
> release mode. You can remove the asserts, but the implicit conversion
> remains. This discourages the use of contracts.
> You can't write contracts which involve more than one parameter.
> Adding new contracts or removing contracts becomes difficult - you have to
> change your wrapper type, or mixin multiple contract wrappers.
> There is more typing overhead involved. Why is it more elegant to have a
> wrapper class than to just have the tooling extract the pre and
> post-conditions from the begging of the method and show them to you in the
> editor and the documentation?
>
> To demonstrate my point, compare the Code Contracts style to the Wrapper
> Type Contract style in the BiggerThanFour exmaple. Here is the original
> BiggerThanFour example:
>
> final case class BiggerThanFour(value: Int) {
>   assert(value > 4)
> }
>
> object BiggerThanFour {
>   implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
>   implicit def take(in: BiggerThanFour): Int = in.value
> }
>
> def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
>   i - j
>
> Here is what it would look like if we just implemented Code Contracts in
> scala (without adding new syntax):
>
> def subtract(i: Int, j: Int): Int = {
>    Requires(i > 4 && j > 4)
>    Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the
> real return value for Result[Int]()
>    i - j
> }
>
> Or, using jaan's suggestion involving new syntax:
> def subtract(i: Int, j: Int): Int
>     Requires(i > 4 && j > 4)
>     Ensures(Result > 4) // assuming the compiler makes Result an Int here
> implicitly
>    = i - j
>
> To me, both of these look more succinct, elegant, and flexible than the
> BiggerThanFour approach.
>
>
> Also, regarding static analysis: In my experience with Code Contracts, I've
> found some situations where the analyzer can't prove a contract has not been
> violated, however the analyzer can tell when it can't prove a contract, and
> will issue a warning to this effect. I found that this happened less often
> than I thought it would. In a project of around 15,000 lines of code, I
> think this happened only three times. To be fair - the project didn't
> dynamically load assemblies or use the dynamic language runtime or any
> similar situation where there is more information available at runtime than
> at compile time.
>
> If this happens, usually there is an obvious reason that you can address
> easily. Otherwise, as a last resort you can insert Assume calls into the
> code to give the analyzer the information it needs to prove a contract
> hasn't been violated. Assume calls are also evaluated and checked at
> run-time to ensure that your assumptions are indeed correct.
>


Meredith Gregory
Joined: 2008-12-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Design By Contract
Dear Adriaan,
i agree. i made similar points in my 2003 ACM paper here.
Best wishes,
--greg

On Mon, Jul 12, 2010 at 10:16 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
From the academic point of view: types and contracts are not that different. Similarly, it would be nice to have a "dial" that determines the intensity of the type checker, which would go from JavaScript to Coq -- all in the same language. Regarding the first point: http://software.imdea.org/~aleks/papers/hoarelogic/jfpsep07.pdf
After reading that, imagine multiplying the expressivity of such a type system by the flexibility of the second point, the orthogonal feature of making a type system "gradual" (or "optional" or "pluggable" -- see ). This should address the concerns that contract-like types become unwieldy, whereas the polymorphism of the type system will ensure that contracts can be reused using standard language features (instead of repeating the mistake of adding something to the language as a second class citizen, and then reinventing polymorphism for it all over again).
adriaan
ps: follow ups welcome, but we should probably grab a beer and move to the debate room

On Mon, Jul 12, 2010 at 4:27 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
Perhaps I should clarify. I don't disagree with the idea that contracts should be part of the "interface". What I was trying to say was that the wrapper class method of implementing contracts as interface has some limitations and drawbacks, among them the fact that they do not actually ensure the contract is fulfilled at compile time.

However, I'm also not saying that a static verifier is the only solution either. The main goal of contracts as interface is to prevent incorrect usage at compile time, and there is more than one path to this goal.

For example, this can be achieved through scala's type system, if you accept certain limitations.  The rocket ship example works quite elegantly, but (correct me if I'm wrong) it relies on the fact that the RocketShip class is immutable.

The static verifier/plugin route is also not without its flaws, but I think it strikes a good practical balance for the general case, when a more elegant solution can't be used.

Regards,
Jeremy Bell


On Mon, Jul 12, 2010 at 4:29 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
I disagree I think a contract is the essence of an interface. Every
interface has a signature which states which types it accepts and it
has certain rules governing its usage. Some of these rules can be
expressed through the type system and others have to be checked by the
implementer but still it is assumed that they are not violated.

Examples:
Monads have laws governing them if they are not fullfilled you do not
have a Monad. These laws can not be guaranteed by the signature but
have to be assured by the implementation (please correct me if this is
false)
Ordered has the assumption that the elements have a stable order. This
is part of the contract. It is expressed by the usage of the Ordered
Trait that you are fullfilling the contract but still the compiler
cannot guarantee that the compare method is correctly implemented.
e.g
class WeirdOrderedInteger(val i: Int) extends Ordered[Int] {
 def compare(i1: Int, i2: Int): Int = {
   val r = Random.nextInt(40)
   if (r == i) 0 else if(r > 20) -1 else 1
 }
}

I think this applies to any DbC as well. So a wrapper type is just a
way of making the contract more explicit and enabling the compiler to
catch violations early on.
Changing the contract therefor is on the same level as changing a
signature or a class it is a change in the underlying interface and
the way the whole system behaves.

-Stefan


2010/7/9 Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com>:
>
>
> On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen
> <daniel [dot] kristensen [at] gmail [dot] com> wrote:
>>
>> I don't need convincing - I think good static analysis is extremely
>> valuable. But when it isn't feasible to check something statically, I think
>> runtime checks are a lot better than nothing. Especially when they're nicely
>> factored into a type with a name clearly expressing the contract as in the
>> BiggerThanFour example.
>>
>> Also, I interpreted the OP's question to be about Design by Contract - not
>> necessarily static analysis. So I think David's example with BiggerThanFour
>> was poerfectly relevant.
>>
>> Cheers,
>> Daniel
>
>
> I'm not completely convinced of the benefits of wrapper types for enforcing
> design contracts over simply implementing the contracts similarly to other
> frameworks, for the following reasons:
>
> First of all, you have to introduce a new type for each contract, or even
> multiple types that get mixed in for multiple contracts. This obfuscates
> your interface for the person that has to use your method. I have to track
> down every implicit conversion for every parameter of your function just to
> figure out what I'm supposed to send to it.
> Wrapper classes with implicit conversions are slow, and using this method it
> is far more difficult to write a plugin that removes the contract checks in
> release mode. You can remove the asserts, but the implicit conversion
> remains. This discourages the use of contracts.
> You can't write contracts which involve more than one parameter.
> Adding new contracts or removing contracts becomes difficult - you have to
> change your wrapper type, or mixin multiple contract wrappers.
> There is more typing overhead involved. Why is it more elegant to have a
> wrapper class than to just have the tooling extract the pre and
> post-conditions from the begging of the method and show them to you in the
> editor and the documentation?
>
> To demonstrate my point, compare the Code Contracts style to the Wrapper
> Type Contract style in the BiggerThanFour exmaple. Here is the original
> BiggerThanFour example:
>
> final case class BiggerThanFour(value: Int) {
>   assert(value > 4)
> }
>
> object BiggerThanFour {
>   implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
>   implicit def take(in: BiggerThanFour): Int = in.value
> }
>
> def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
>   i - j
>
> Here is what it would look like if we just implemented Code Contracts in
> scala (without adding new syntax):
>
> def subtract(i: Int, j: Int): Int = {
>    Requires(i > 4 && j > 4)
>    Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the
> real return value for Result[Int]()
>    i - j
> }
>
> Or, using jaan's suggestion involving new syntax:
> def subtract(i: Int, j: Int): Int
>     Requires(i > 4 && j > 4)
>     Ensures(Result > 4) // assuming the compiler makes Result an Int here
> implicitly
>    = i - j
>
> To me, both of these look more succinct, elegant, and flexible than the
> BiggerThanFour approach.
>
>
> Also, regarding static analysis: In my experience with Code Contracts, I've
> found some situations where the analyzer can't prove a contract has not been
> violated, however the analyzer can tell when it can't prove a contract, and
> will issue a warning to this effect. I found that this happened less often
> than I thought it would. In a project of around 15,000 lines of code, I
> think this happened only three times. To be fair - the project didn't
> dynamically load assemblies or use the dynamic language runtime or any
> similar situation where there is more information available at runtime than
> at compile time.
>
> If this happens, usually there is an obvious reason that you can address
> easily. Otherwise, as a last resort you can insert Assume calls into the
> code to give the analyzer the information it needs to prove a contract
> hasn't been violated. Assume calls are also evaluated and checked at
> run-time to ensure that your assumptions are indeed correct.
>





--
L.G. Meredith
Managing Partner
Biosimilarity LLC
1219 NW 83rd St
Seattle, WA 98117

+1 206.650.3740

http://biosimilarity.blogspot.com
kravets
Joined: 2008-08-20,
User offline. Last seen 2 years 10 weeks ago.
Re: Re: Design By Contract

Sage Programming Language has a powerful and novel perspective on this subject http://sage.soe.ucsc.edu/.

On Mon, Jul 12, 2010 at 10:16 AM, Adriaan Moors <adriaan [dot] moors [at] epfl [dot] ch> wrote:
From the academic point of view: types and contracts are not that different. Similarly, it would be nice to have a "dial" that determines the intensity of the type checker, which would go from JavaScript to Coq -- all in the same language. Regarding the first point: http://software.imdea.org/~aleks/papers/hoarelogic/jfpsep07.pdf
After reading that, imagine multiplying the expressivity of such a type system by the flexibility of the second point, the orthogonal feature of making a type system "gradual" (or "optional" or "pluggable" -- see ). This should address the concerns that contract-like types become unwieldy, whereas the polymorphism of the type system will ensure that contracts can be reused using standard language features (instead of repeating the mistake of adding something to the language as a second class citizen, and then reinventing polymorphism for it all over again).
adriaan
ps: follow ups welcome, but we should probably grab a beer and move to the debate room

On Mon, Jul 12, 2010 at 4:27 PM, Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com> wrote:
Perhaps I should clarify. I don't disagree with the idea that contracts should be part of the "interface". What I was trying to say was that the wrapper class method of implementing contracts as interface has some limitations and drawbacks, among them the fact that they do not actually ensure the contract is fulfilled at compile time.

However, I'm also not saying that a static verifier is the only solution either. The main goal of contracts as interface is to prevent incorrect usage at compile time, and there is more than one path to this goal.

For example, this can be achieved through scala's type system, if you accept certain limitations.  The rocket ship example works quite elegantly, but (correct me if I'm wrong) it relies on the fact that the RocketShip class is immutable.

The static verifier/plugin route is also not without its flaws, but I think it strikes a good practical balance for the general case, when a more elegant solution can't be used.

Regards,
Jeremy Bell


On Mon, Jul 12, 2010 at 4:29 AM, Stefan Langer <mailtolanger [at] googlemail [dot] com> wrote:
I disagree I think a contract is the essence of an interface. Every
interface has a signature which states which types it accepts and it
has certain rules governing its usage. Some of these rules can be
expressed through the type system and others have to be checked by the
implementer but still it is assumed that they are not violated.

Examples:
Monads have laws governing them if they are not fullfilled you do not
have a Monad. These laws can not be guaranteed by the signature but
have to be assured by the implementation (please correct me if this is
false)
Ordered has the assumption that the elements have a stable order. This
is part of the contract. It is expressed by the usage of the Ordered
Trait that you are fullfilling the contract but still the compiler
cannot guarantee that the compare method is correctly implemented.
e.g
class WeirdOrderedInteger(val i: Int) extends Ordered[Int] {
 def compare(i1: Int, i2: Int): Int = {
   val r = Random.nextInt(40)
   if (r == i) 0 else if(r > 20) -1 else 1
 }
}

I think this applies to any DbC as well. So a wrapper type is just a
way of making the contract more explicit and enabling the compiler to
catch violations early on.
Changing the contract therefor is on the same level as changing a
signature or a class it is a change in the underlying interface and
the way the whole system behaves.

-Stefan


2010/7/9 Jeremy Bell <bell [dot] jeremy [at] gmail [dot] com>:
>
>
> On Fri, Jul 9, 2010 at 7:25 AM, Daniel Kristensen
> <daniel [dot] kristensen [at] gmail [dot] com> wrote:
>>
>> I don't need convincing - I think good static analysis is extremely
>> valuable. But when it isn't feasible to check something statically, I think
>> runtime checks are a lot better than nothing. Especially when they're nicely
>> factored into a type with a name clearly expressing the contract as in the
>> BiggerThanFour example.
>>
>> Also, I interpreted the OP's question to be about Design by Contract - not
>> necessarily static analysis. So I think David's example with BiggerThanFour
>> was poerfectly relevant.
>>
>> Cheers,
>> Daniel
>
>
> I'm not completely convinced of the benefits of wrapper types for enforcing
> design contracts over simply implementing the contracts similarly to other
> frameworks, for the following reasons:
>
> First of all, you have to introduce a new type for each contract, or even
> multiple types that get mixed in for multiple contracts. This obfuscates
> your interface for the person that has to use your method. I have to track
> down every implicit conversion for every parameter of your function just to
> figure out what I'm supposed to send to it.
> Wrapper classes with implicit conversions are slow, and using this method it
> is far more difficult to write a plugin that removes the contract checks in
> release mode. You can remove the asserts, but the implicit conversion
> remains. This discourages the use of contracts.
> You can't write contracts which involve more than one parameter.
> Adding new contracts or removing contracts becomes difficult - you have to
> change your wrapper type, or mixin multiple contract wrappers.
> There is more typing overhead involved. Why is it more elegant to have a
> wrapper class than to just have the tooling extract the pre and
> post-conditions from the begging of the method and show them to you in the
> editor and the documentation?
>
> To demonstrate my point, compare the Code Contracts style to the Wrapper
> Type Contract style in the BiggerThanFour exmaple. Here is the original
> BiggerThanFour example:
>
> final case class BiggerThanFour(value: Int) {
>   assert(value > 4)
> }
>
> object BiggerThanFour {
>   implicit def make(in: Int): BiggerThanFour = new BiggerThanFour(in)
>   implicit def take(in: BiggerThanFour): Int = in.value
> }
>
> def subtract(i: BiggerThanFour, j: BiggerThanFour): BiggerThanFour =
>   i - j
>
> Here is what it would look like if we just implemented Code Contracts in
> scala (without adding new syntax):
>
> def subtract(i: Int, j: Int): Int = {
>    Requires(i > 4 && j > 4)
>    Ensures(Result[Int]() > 4) // plugin moves this code and substitutes the
> real return value for Result[Int]()
>    i - j
> }
>
> Or, using jaan's suggestion involving new syntax:
> def subtract(i: Int, j: Int): Int
>     Requires(i > 4 && j > 4)
>     Ensures(Result > 4) // assuming the compiler makes Result an Int here
> implicitly
>    = i - j
>
> To me, both of these look more succinct, elegant, and flexible than the
> BiggerThanFour approach.
>
>
> Also, regarding static analysis: In my experience with Code Contracts, I've
> found some situations where the analyzer can't prove a contract has not been
> violated, however the analyzer can tell when it can't prove a contract, and
> will issue a warning to this effect. I found that this happened less often
> than I thought it would. In a project of around 15,000 lines of code, I
> think this happened only three times. To be fair - the project didn't
> dynamically load assemblies or use the dynamic language runtime or any
> similar situation where there is more information available at runtime than
> at compile time.
>
> If this happens, usually there is an obvious reason that you can address
> easily. Otherwise, as a last resort you can insert Assume calls into the
> code to give the analyzer the information it needs to prove a contract
> hasn't been violated. Assume calls are also evaluated and checked at
> run-time to ensure that your assumptions are indeed correct.
>





--
Alex Kravets      (define red-pill 'lisp)
[[ brutal honesty is the best policy ]]

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland