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; Mon, 25 Oct 1993 22:37:07 +0000 Received: by leopard.cs.byu.edu (1.37.109.4/16.2) id AA21982; Mon, 25 Oct 93 16:26:15 -0600 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from panther.cs.byu.edu by leopard.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA21978; Mon, 25 Oct 93 16:26:15 -0600 Received: from localhost by panther.cs.byu.edu with SMTP (1.37.109.4/16.2) id AA29774; Mon, 25 Oct 93 16:26:14 -0600 To: Chris Toshok Cc: info-hol@leopard.cs.byu.edu Subject: Re: Specification languages in HOL In-Reply-To: Your message of Mon, 25 Oct 1993 12:52:01 -0700. <199310251952.AA09466@panther.cs.uidaho.edu> Date: Mon, 25 Oct 1993 16:26:13 -0600 From: Phil Windley Message-ID: <"swan.cl.cam.:076020:931025223753"@cl.cam.ac.uk> On Mon, 25 Oct 1993 12:52:01 -0700 Chris Toshok writes +-------------------- | I was wondering if there had been any work done in HOL with any | specification languages (Z for example). I am looking specifically for | references or information on verifying code by way of a semantic | description and a specification. Any information would be greatly | appreciated. Chris, Phil Weiss (weiss@panther.cs.uidaho.edu) and I were doing some work in this area a while back. We had taken a Z based semantics of Linda and translated it into HOL. Along the way, we came up with some rules for doing this. Unfortunately, none of it was finished or published. Your best bet is to contact Phil directly and see if he can give you his files and what he has written up. Cheers, --phil-- Phillip J. Windley, Asst. Professor | windley@cs.byu.edu Laboratory for Applied Logic | Dept. of Computer Science, TMCB 3370 | Brigham Young University | Phone: 801.378.3722 Provo UT 84602-6576 | Fax: 801.378.7775