Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 13 May 1993 11:00:59 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA17606; Thu, 13 May 93 02:47:31 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA17601; Thu, 13 May 93 02:47:24 -0700 Received: from skua.cl.cam.ac.uk (user pjv1000 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 13 May 1993 10:41:55 +0100 To: Mike Coe Cc: info-hol@ted.cs.uidaho.edu Subject: Re: wp and Hoare logic In-Reply-To: Your message of "Mon, 10 May 93 09:38:01 PDT." <199305101638.AA19935@panther.cs.uidaho.edu> Date: Thu, 13 May 93 10:41:46 +0100 From: Joakim von Wright Message-Id: <"swan.cl.cam.:044490:930513094201"@cl.cam.ac.uk> There is a contrib-contribution RefCalc coming in version 2.2. It is concerned with total correctness and program refinement within a framework which extends Dijkstra's wp calculus considerably. I hope to get a proper documentation of RefCalc finished this summer. The following references describe some of the basic ideas: @INPROCEEDINGS(WrSe91, AUTHOR = " J. von Wright and K. Sere", TITLE = "Program Transformations and Refinements in {HOL}", BOOKTITLE = "Proc.\ 1991 International Workshop on Higher Order Logic Theorem Proving and its Applications", YEAR = 1991, publisher = {IEEE/ACM}, address = "Davis, USA", month = "August" ) @INPROCEEDINGS(WHLL92, AUTHOR = "J. von Wright, J. Hekanaho, T. L{\aa}ngbacka, P. Luostarinen", TITLE = "Mechanising some Advanced Refinement Concepts", BOOKTITLE = "Proc.\ 1992 International Workshop on Higher Order Logic Theorem Proving and its Applications", YEAR = 1992, publisher = {North-Holland}, address = "Leuven, Belgium", month = "September" ) Joakim von Wright