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.

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.

Hendrik