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=0.0 required=5.0 tests=none 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 16507BC0B for ; Sun, 4 Feb 2007 16:47:50 +0100 (CET) Received: from smtp19.orange.fr (smtp19.orange.fr [80.12.242.17]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l14Fln3L017746 for ; Sun, 4 Feb 2007 16:47:49 +0100 Received: from me-wanadoo.net (localhost [127.0.0.1]) by mwinf1907.orange.fr (SMTP Server) with ESMTP id 88F691C00095; Sun, 4 Feb 2007 16:47:49 +0100 (CET) Received: from morgana (ARennes-257-1-64-247.w81-53.abo.wanadoo.fr [81.53.143.247]) by mwinf1907.orange.fr (SMTP Server) with ESMTP id 562781C00092; Sun, 4 Feb 2007 16:47:49 +0100 (CET) X-ME-UUID: 20070204154749352.562781C00092@mwinf1907.orange.fr Received: from david by morgana with local (Exim 4.50) id 1HDjam-0001NQ-Bz; Sun, 04 Feb 2007 16:47:48 +0100 To: oleg@pobox.com Cc: caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si Subject: Design-by-contract and Type inference? References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> From: David MENTRE Organization: none Date: Sun, 04 Feb 2007 16:47:48 +0100 In-Reply-To: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> (oleg@pobox.com's message of "Wed, 31 Jan 2007 21:04:31 -0800 (PST)") Message-ID: <87fy9lhql7.fsf@linux-france.org> User-Agent: Gnus/5.1006 (Gnus v5.10.6) Emacs/21.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Miltered: at discorde with ID 45C60025.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; inference:01 oleg:01 oleg:01 larus:01 abadi:01 pointers:01 invariants:01 inference:01 ocaml:01 compiler:01 statically:01 gpg:01 mart:98 murphy:98 writes:01 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