Design-by-contract and Type inference?

[David MENTRE <dmentre@linux-france.org>]

Hello Oleg,

oleg@pobox.com writes:

> @Book{		barnes-high,
>   author	= "John Barnes",
>   title		= "High Integrity Software: 
>                     The {SPARK} Approach to Safety and Security",
[...]
> @TechReport{	hunt-singularity,
>   author	= "Galen Hunt and James R. Larus and Mart{\'\i}n Abadi and 
>         Mark Aiken and Paul Barham and Manuel F{\"a}hndrich and
>         Chris Hawblitzel and Orion Hodson and Steven Levi and
>         Nick Murphy and Bjarne Steensgaard and David Tarditi and
>         Ted Wobber and Brian D. Zill",
>   title		= "An Overview of the {S}ingularity Project",

Thank you for those interesting pointers. Interestingly both Spark
language and Sing# language used in Singularity contains
Design-by-Contract-like features (pre- and post-conditions, invariants,
...). 

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.

Best wishes,
d.
-- 
GPG/PGP key: A3AD7A2A David MENTRE <dmentre@linux-france.org>
 5996 CC46 4612 9CA4 3562  D7AC 6C67 9E96 A3AD 7A2A