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 7D747BC69 for ; Tue, 6 Feb 2007 21:45:15 +0100 (CET) Received: from einhorn.in-berlin.de (einhorn.in-berlin.de [192.109.42.8]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l16KjEuM029475 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Tue, 6 Feb 2007 21:45:15 +0100 X-Envelope-From: oliver@first.in-berlin.de X-Envelope-To: Received: from first (d102245.adsl.hansenet.de [80.171.102.245]) (authenticated bits=0) by einhorn.in-berlin.de (8.13.6/8.13.6/Debian-1) with ESMTP id l16KjD4x019187 for ; Tue, 6 Feb 2007 21:45:14 +0100 Received: by first (Postfix, from userid 501) id A7E1836BEC4; Tue, 6 Feb 2007 21:45:07 +0100 (CET) Date: Tue, 6 Feb 2007 21:45:07 +0100 From: Oliver Bandel To: caml-list@inria.fr Subject: Re: [Caml-list] Design-by-contract and Type inference? Message-ID: <20070206204507.GV331@first.in-berlin.de> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <87fy9lhql7.fsf@linux-france.org> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: User-Agent: Mutt/1.5.6i X-Scanned-By: MIMEDefang_at_IN-Berlin_e.V. on 192.109.42.8 X-Miltered: at concorde with ID 45C8E8DA.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; bandel:01 in-berlin:01 inference:01 0100,:01 hendrik:01 tews:01 inference:01 ocaml:01 compiler:01 statically:01 ocaml's:01 mli-files:01 sig:01 compilation:01 compiler:01 Hello, On Tue, Feb 06, 2007 at 10:29:10AM +0100, Hendrik Tews wrote: > 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. As far as I know (but I only have seen some simple examples of it), Design by contract is a way, to make a contract between people (or for one developer with himself/herself) so that there is an interface, that will be agreed on. This is only text with no effect on the code, something like an interface-description inside comments. (But maybe it can also be used in different ways, which I don#t know). As far as I can see, the OCaml's module system (with module-keyword, or mli-files) offers a contract also, but one, that also has effect on the program, and is not only comment: editing the signature in a "sig ... end" or in an mli-file directly has effect on what can be seen from the outside of that module. And that is a contract which necessarily must be accepted. It's more than only a comment. It's working code. If you also use abstract types, then it's also not possible to make awful things inside a module/compilation unit. > > 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. [...] You can use the compiler to give you the signature. For example $ ocamlc -i example.ml Will give you the signature of your file. But ifyou have narrowed the signature by explicitly doing it with "sig ... end", then only the explicit signature will be shown. Letting the compiler show the signature of your compilation unit can help a lot in providing *.mli files. In the above example, it could be done with $ ocamlc -i example.ml > example.mli and afterwards you can edit the mli-file. And the mli-file could be used in a team of developers in a way that only certain people coulkd edit it, so that nothing can become broken. Than the interface is valid and all developers have to use it. Ciao, Oliver