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 7C197BC69 for ; Tue, 6 Feb 2007 22:35:57 +0100 (CET) Received: from lion.seas.upenn.edu (LION.SEAS.upenn.edu [158.130.12.194]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l16LZt98029805 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Tue, 6 Feb 2007 22:35:57 +0100 Received: from [158.130.12.234] (GRW74-1.CIS.upenn.edu [158.130.12.234]) (authenticated bits=0) by lion.seas.upenn.edu (8.13.6/8.13.6) with ESMTP id l16LZp6u007368 (version=TLSv1/SSLv3 cipher=AES128-SHA bits=128 verify=NOT); Tue, 6 Feb 2007 16:35:51 -0500 In-Reply-To: <20070206204507.GV331@first.in-berlin.de> References: <20070201050431.E278AAB40@Adric.metnet.fnmoc.navy.mil> <87fy9lhql7.fsf@linux-france.org> <20070206204507.GV331@first.in-berlin.de> Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed Message-Id: <7009B5BE-ABF2-42B7-9419-84B48ECD4A25@seas.upenn.edu> Cc: caml-list@inria.fr Content-Transfer-Encoding: 7bit From: Alwyn Goodloe Subject: Re: [Caml-list] Design-by-contract and Type inference? Date: Tue, 6 Feb 2007 16:35:45 -0500 To: Oliver Bandel X-Mailer: Apple Mail (2.752.2) X-Miltered: at discorde with ID 45C8F4BB.006 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; alwyn:01 goodloe:01 inference:01 haskell:01 haskell:01 ocaml:01 alwyn:01 bandel:01 0100,:01 hendrik:01 tews:01 inference:01 ocaml:01 compiler:01 statically:01 In a related note I believe a student at Cambridge University has done some work on ESC/Haskell that would support design by contract for Haskell. This leads one to believe that one could probably build a version of ESC for OCAML. Alwyn On Feb 6, 2007, at 3:45 PM, Oliver Bandel wrote: > 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 > > _______________________________________________ > 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