Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Programming with correctness guarantees
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-02-06 (21:35)
From: Alwyn Goodloe <agoodloe@s...>
Subject: Re: [Caml-list] Design-by-contract and Type inference?
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.


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 <> 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
> 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.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:
> Archives:
> Beginner's list:
> Bug reports: