Re: Contracts (feature request)

Hi,


In my paper "Scala and AsmL side by side" (May 2003) available from:

  http://www.scala-lang.org/docu/related.html#techreports


you'll find an implementation of pre/post conditions based
on the require/ensure construct from the AsmL language (Microsoft):

  "Functions in AsmL may contain both pre- and post-conditions;
   the require and ensure statements document constraints placed
   upon the model. Violating a constraint at runtime is called
   an assertion failure and indicates a modeling error. In a
   post-condition the name result refers to the value of the
   block which contains the pre- and post-conditions."


Here is the Scala code example:

object Main {
  trait Ensure[A] {
    def ensure(postcondition: A => Boolean): A
  }
  def require[A](precondition: => Boolean)(command: => A): Ensure[A] =
    if (precondition)
      new Ensure[A] {
        def ensure(postcondition: A => Boolean): A = {
          val result = command
          if (postcondition(result)) result
          else error("Assertion error")
        }
      }
    else
      error("Assertion error")
  def main(args: Array[String]) {
    def fun[a](s: List[a]) =
      require (! s.isEmpty) {
        s.head
      } ensure (result => s contains result)
    val xs = List(1, 2)
    Console.println("xs=" + xs + ", " + fun(xs))
  }
}


Bye
--Stephane


Henrik Huttunen wrote:
> Hi all,
> 
> I'm quite new to Scala and like a lot its approach to support programmer.
> It has obviously a focus on scalable component programming
> (provided/required services and mixin composition). That's why I would
> almost expect to see contracts integrated into the language.
> By contracts I mean pre- and post conditions for methods and a class
> invariant, which all are checked at runtime (precondition and class
> invariant before invocation of the body of the method and postcondition
> and class invariant after leaving the method).
> The reason why I think those are important, is that seperating the
> contract from body makes the code a bit less burdensome to read. For
> instance, pre and post have different meaning, they're not just any
> asserts. Also postcondition test is not needed in different exit paths
> of method (wrapping method call isn't a good alternative either).
> One big advantage is that the conditions are spread to subclasses
> automatically by compiler.
> 
> Is there any plans for this, or am I just dreaming of a thing that just
> don't fit in Scala?
> 
> Example:
> 
> def fun(x: Int): Int
>   pre{
>     x >= 0 && x < 10
>   }
>   post(result){
>     result < x
>   }
>   = {
>     -x
>   }
> 
> Thanks for very interesting language!
> Sincerely, Henrik
>