Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from toadflax.cs.ucdavis.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <27941-0@swan.cl.cam.ac.uk>; Mon, 20 Jan 1992 17:29:32 +0000
Received: from swan.cl.cam.ac.uk by toadflax.cs.ucdavis.edu (4.1/UCD.CS.1.0)
          id AA05439; Mon, 20 Jan 92 09:14:12 PST
Received: from pochard.cl.cam.ac.uk by swan.cl.cam.ac.uk
          with SMTP (PP-6.0) to cl id <27275-0@swan.cl.cam.ac.uk>;
          Mon, 20 Jan 1992 17:01:56 +0000
To: ramu@com.mot.corp.cadsun
Cc: info-hol@edu.ucdavis.cs
Subject: Re: Query about testing
In-Reply-To: Your message of Mon, 20 Jan 92 10:06:56 -0600. <9201201606.AA17227@cadsun.corp.mot.com>
Date: Mon, 20 Jan 92 17:01:47 +0000
From: Juanito.Camilleri@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.280:20.00.92.17.01.58"@cl.cam.ac.uk>




> Ramu@mot.com  writes.....

> Given a specification of system, can a theorem prover be used at any
> stage to perform specification-dependent testing?  Formal testing is
> mostly like to fault-detection, where one wants to detect undesirable
> states of a computation.

> I'd welcome pointers to published papers or technical reports in this
> area.



I have just published the following technical report which may be
of interest...


Title:     Symbolic Compilation and Execution of Programs
                    by Proof: a case study in HOL

                         Tech. Report No 240
                           (December 1991)
                         Computer Laboratory
                       University of Cambridge


                               ABSTRACT

This paper illustrates the symbolic `compilation' and  `execution'
of programs by proof using the proof assistant HOL. We formalise
the operational semantics of an occam-like programming language Oc
and show how synchronous communication in Oc compiles to an intermediate
programming language SAFE whose compilation yields instructions intended
to drive machines that communicate via shared memory. We show how the
symbolic formal manipulation of terms of a programming language, subject
to the definition of its semantics, can "animate" a desired effect---be
it compilation or execution. Needless to say, such compilation and execution
by proof is rather slow, but it is fast enough to give vital feedback about
the compilation algorithm being used. Without such animation it is hard to
anticipate whether the compilation algorithm is reasonable before attempting
to verify it. This is particularly true when attempting to find a plausible
handshaking protocol that implements synchronous communication.


Cheers
Juanito