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

[Oliver Bandel <oliver@first.in-berlin.de>]

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