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, 26 Oct 1993 09:16:18 +0000 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA25972; Tue, 26 Oct 93 03:01:47 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA25968; Tue, 26 Oct 93 03:01:44 -0600 Received: from relay1.pipex.net by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA15401; Tue, 26 Oct 93 01:58:44 -0700 Received: from Q.icl.co.uk by relay1.pipex.net with SMTP (PP) id <02968-0@relay1.pipex.net>; Tue, 26 Oct 1993 08:58:18 +0000 Received: from ming.oasis.icl.co.uk by Q.icl.co.uk (4.1/icl-2.8-server) id AA21803; Tue, 26 Oct 93 09:59:48 BST Received: on ming.oasis.icl.co.uk over UUCP id AA14962; Tue, 26 Oct 93 09:58:29 BST From: Roger Bishop Jones Date: Tue, 26 Oct 93 08:43:52 GMT Message-Id: <9310260843.20020.0@norman.win.icl.co.uk> To: info-hol@cs.uidaho.edu Subject: Re: Specification Languages in HOL ProofPower provides proof support for Z via a semantic embedding of Z into HOL. We have also done work enabling the verification of pre- and post-conditions expressed in SAL (SPARK Annotation Language, SPARK is a subset of Ada supported by verification tools marketed by Program Validation Limited) against specifications in Z, which gives a route through to verified Ada using ProofPower in conjunction with the PVL SPARK Analyser and proof tool. Support for SAL in ProofPower has however not yet found its way into any issued product. Information on ProofPower can be obtained from an email server addressed as: ProofPower-server@win.icl.co.uk send any message and it will respond with help info. Roger Jones International Computers Limited