From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.4 required=5.0 tests=HTML_MESSAGE,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 9B2B2BC0B for ; Sun, 4 Feb 2007 17:04:58 +0100 (CET) Received: from wr-out-0506.google.com (wr-out-0506.google.com [64.233.184.237]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l14G4vD4020655 for ; Sun, 4 Feb 2007 17:04:58 +0100 Received: by wr-out-0506.google.com with SMTP id i28so1020031wra for ; Sun, 04 Feb 2007 08:04:57 -0800 (PST) DomainKey-Signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:references:x-google-sender-auth; b=Xs8RUZ3Twa4de0N+TbgZyLlS5Ao+tnwkDLyOs8iYiGcR6FpAXbdSbCri6GpKb0lS4IxZEBFMkY9TMDMvgZhqjnuWQxK9GG2fCOYSe/VGrcEDxrOJE6aBgN9qdSH7VCHQ+p4XJ+P6eMGLwG0AxBMieyRo8Oi4n/6WTUYWcGDTOCQ= Received: by 10.115.93.16 with SMTP id v16mr519254wal.1170605096349; Sun, 04 Feb 2007 08:04:56 -0800 (PST) Received: by 10.114.25.10 with HTTP; Sun, 4 Feb 2007 08:04:56 -0800 (PST) Message-ID: <9b415f950702040804o3a118512j112263536d1e0589@mail.gmail.com> Date: Sun, 4 Feb 2007 17:04:56 +0100 From: "Benedikt Grundmann" Sender: benedikt.grundmann@googlemail.com To: "David MENTRE" Subject: Re: [Caml-list] Design-by-contract and Type inference? Cc: oleg@pobox.com, caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si In-Reply-To: <87fy9lhql7.fsf@linux-france.org> MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_16196_1130467.1170605096285" References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <87fy9lhql7.fsf@linux-france.org> X-Google-Sender-Auth: 8f6a35c1c751b189 X-Miltered: at discorde with ID 45C60429.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; grundmann:01 inference:01 inference:01 cheers:01 oleg:01 oleg:01 larus:01 abadi:01 pointers:01 invariants:01 ocaml:01 compiler:01 statically:01 gpg:01 beginner's:01 X-Attachments: cset="UTF-8" cset="UTF-8" ------=_Part_16196_1130467.1170605096285 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Content-Disposition: inline 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 : > > 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 > 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 > ------=_Part_16196_1130467.1170605096285 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: 7bit Content-Disposition: inline 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

------=_Part_16196_1130467.1170605096285--