Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 28 Feb 1995 08:42:06 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA094089906; Tue, 28 Feb 1995 01:25:06 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from iraun1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA094039896; Tue, 28 Feb 1995 01:24:56 -0700 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Tue, 28 Feb 1995 09:23:08 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <20104-0@i80fs2.ira.uka.de>; Tue, 28 Feb 1995 09:23:03 +0100 Date: Tue, 28 Feb 95 9:23:02 EST From: reetz To: terra@APL.FOX.CS.CMU.EDU Cc: info-hol@leopard.cs.byu.edu Subject: Re: Need real-world Hol-90 proofs running for 5-60 minutes Message-Id: <"i80fs2.ira.106:28.02.95.08.23.03"@ira.uka.de> >I need real-world[tm] examples of Hol-90 For a real-world example, define derivation trees as a syntax representation in Hol-90 for the IEEE Standard hardware description language VHDL using the method shown in [ReKr94]. Even for a subset with a context--free grammar consisting of 46 terminals and 187 production rules, the SECURE definition needed 2 days, 600 MB heapsize on a Sparc 10 with 128 MB main memory. The unsecure definition, i.e. just introducing the types and type constructors needed a few seconds. Put it more generally: take the library generator, formalize a real-word language and, (automatically) prove the semantics of a concrete large program. Or take a closer look at the two examples delivered with the library generator. You can get arbitrary large examples just by setting ONE parameter and you even get reports on used time and rules automatically. Or wait for the next version of the library generator, maybe including that VHDL subset....... O.k., enough advertisement ;-) - the library more_utils contains functions in order to generate these benchmarks easily. In my personal experience it is not difficult to drive Hol to the edge, especially to the memory-consumption edge. But be aware who is to blame for that: the hol logic itself? the implementation of Hol-90? the SML used? IMHO there is no unique answer, but maybe worth a discussion here... Ralf. (**************************************************************) (* *) (* Ralf Reetz *) (* *) (* University of Karlsruhe *) (* Institut fuer Rechnerentwurf und Fehlertoleranz *) (* 76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany *) (* *) (* e-mail: reetz@ira.uka.de *) (* WWW: http://goethe.ira.uka.de/people/reetz/reetz.html *) (* *) (**************************************************************)