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

["Benedikt Grundmann" <benedikt@cardexpert.net>]

[-- Attachment #1: Type: text/plain, Size: 2201 bytes --]

Hello

Well a lot of the stuff you express with DBC can be expressed using
dependent types (Array indices are a popular example).  You should take that
in account in your search for papers (If I recall correctly there are quite
a few papers on combining dependent types and (at the very least
partial/local) type inference).

Cheers,

Bene

2007/2/4, 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
>
> _______________________________________________
> 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
>

[-- Attachment #2: Type: text/html, Size: 3518 bytes --]