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 concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id 01FBDBC0B for ; Tue, 6 Feb 2007 10:29:15 +0100 (CET) Received: from smeltpunt.science.ru.nl (smeltpunt.science.ru.nl [131.174.16.145]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l169TEjX005066 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Tue, 6 Feb 2007 10:29:14 +0100 Received: from tandem.cs.ru.nl [131.174.142.18] (helo=tandem.cs.ru.nl) by smeltpunt.science.ru.nl (8.13.7/5.11) with ESMTP id l169TABf010335; Tue, 6 Feb 2007 10:29:10 +0100 (MET) Received: from tews by tandem.cs.ru.nl with local (Exim 4.63) (envelope-from ) id 1HEMdS-0002XB-38; Tue, 06 Feb 2007 10:29:10 +0100 From: Hendrik Tews To: David MENTRE Cc: oleg@pobox.com, caml-list@inria.fr, Andrej.Bauer@fmf.uni-lj.si Subject: Re: [Caml-list] Design-by-contract and Type inference? References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <87fy9lhql7.fsf@linux-france.org> Date: Tue, 06 Feb 2007 10:29:10 +0100 In-Reply-To: <87fy9lhql7.fsf@linux-france.org> (David MENTRE's message of "Sun, 04 Feb 2007 16:47:48 +0100") Message-ID: User-Agent: Gnus/5.110006 (No Gnus v0.6) Emacs/21.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Scanned-By: MIMEDefang 2.56 on 131.174.16.145 X-Miltered: at concorde with ID 45C84A6A.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; hendrik:01 tews:01 tews:01 inference:01 inference:01 ocaml:01 compiler:01 statically:01 hendrik:01 caml-list:01 writes:01 static:03 programmer:06 infer:07 mechanisms:07 David MENTRE 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