Re: [Caml-list] Design-by-contract and Type inference?

From: Alwyn Goodloe <agoodloe@seas.upenn.edu>
To: Oliver Bandel <oliver@first.in-berlin.de>
Cc: caml-list@inria.fr
Subject: Re: [Caml-list] Design-by-contract and Type inference?
Date: Tue, 6 Feb 2007 16:35:45 -0500	[thread overview]
Message-ID: <7009B5BE-ABF2-42B7-9419-84B48ECD4A25@seas.upenn.edu> (raw)
In-Reply-To: <20070206204507.GV331@first.in-berlin.de>

In a related note I believe a student at Cambridge University
has done some work on ESC/Haskell that would support
design by contract for Haskell. This leads one to believe that
one could probably build a version of ESC for OCAML.

Alwyn

On Feb 6, 2007, at 3:45 PM, Oliver Bandel wrote:

> Hello,
>
>
> On Tue, Feb 06, 2007 at 10:29:10AM +0100, Hendrik Tews wrote:
>> David MENTRE <dmentre@linux-france.org> writes:
>>
>>    Does anybody know if there is research on design-by-contract  
>> (as used in
>>    Eiffel or Spark) and type inference (as used in OCaml)? For  
>> example,
>>    relationships between both mechanisms, how the compiler could  
>> infer
>>    contracts for a sub-class of a class, how contracts can be  
>> maintained
>>    with minimal work from the programmer (a very useful property  
>> of ML type
>>    inference), how contract can be statically checked using type  
>> inference
>>    information, etc.
>
>
> As far as I know (but I only have seen some simple examples of it),
> Design by contract is a way, to make a contract between people
> (or for one developer with himself/herself) so that there is an
> interface, that will be agreed on.
>
> This is only text with no effect on the code, something like
> an interface-description inside comments.
>
> (But maybe it can also be used in different ways, which I don#t know).
>
> As far as I can see, the OCaml's module system (with module-keyword,
> or mli-files) offers a contract also, but one, that also has effect
> on the program, and is not only comment: editing the signature
> in a   "sig ... end" or in an mli-file directly has effect
> on what can be seen from the outside of that module.
>
> And that is a contract which necessarily must be accepted.
> It's more than only a comment. It's working code.
>
> If you also use abstract types, then it's also not possible
> to make awful things inside a module/compilation unit.
>
>>
>> JML for Java is similar to what Eiffel provides. There are a lot
>> of tools for JML, for instance ESC/Java for automatics static
>> checks.
> [...]
>
> You can use the compiler to give you the
> signature.
>
> For example
>
> $ ocamlc -i example.ml
>
> Will give you the signature of your file.
> But ifyou have narrowed the signature by explicitly
> doing it with "sig ... end", then only the explicit
> signature will be shown.
>
> Letting the compiler show the signature of your compilation
> unit can help a lot in providing *.mli files.
>
> In the above example, it could be done with
>
> $ ocamlc -i example.ml > example.mli
>
> and afterwards you can edit the mli-file.
>
> And the mli-file could be used in a team of developers
> in a way that only certain people coulkd edit it, so
> that nothing can become broken.
> Than the interface is valid and all developers have to use it.
>
> Ciao,
>    Oliver
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs