Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <199212111637.AA04707@panther.cs.uidaho.edu>
To: "Tim Leonard, DTN 225-5809, HLO2-3/C11" <leonard@com.dec.enet.ricks>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Cartesian sums for alternative representations
In-Reply-To: Your message of Fri, 11 Dec 92 10:25:13 -0500. <9212111502.AA08489@easynet.crl.dec.com>
Date: Fri, 11 Dec 92 08:37:19 -0800
From: Phil Windley <windley@edu.uidaho.cs.panther>


Tim,

My impression from what you wrote is that you're more concerned (right now)
with specification than verification.  Also, I assume that you're familiar
with the use of abstract n-bit words that Jeff Joyce pioneered and others
(including me) have profitably used.  Abstract n-bit words will help in the
verification, but don't help with what you seem to be saying:

On Fri, 11 Dec 92 10:25:13 EST, Tim (leonard@ricks.enet.dec.com) wrote:
+------------
| I've been working on the formal spec of the Alpha AXP architecture.  Alpha is
| a 64-bit architecture, and I've been unhappy with all the representations I'v
| considered for 64-bit words.  No matter what I pick --- 64-element lists, or
| 64-tuples, or num, or whatever --- some operations are a real pain, and requi
| converting to and from a more tractable representation.  To do a floating-poi
| operation, for example, I have to convert each word into a real, perform the
| operation, and convert back.
 
From this, I presume that what is bothering you is the *way* your
specifications read---lots of conversions int he specification cluttering
it up. 

| Yesterday it occurred to me that I could use a Cartesian sum:
|   (bool list) + (num) + (int) + (real) + ...

|Are there difficulties with it that I've overlooked?

I would advise against using coproducts (sums) since your spec will be
filled with injections and projections rather than conversions.  Usually,
however, you can use an abstract data type to define the same thing:

define_type `values` 
            `values = WordV bool list | NumV num | IntV int | RealV real`;;

I say usualy, because I ran into a situation just a few weeks ago where for
simplicity I started with coproducts and then later tried to make
everything neater by using abstract data types and discovered that they
weren't saying EXACTLY the same thing in the context I was using them.  If
you're interested, I can write more on this.

The verification, of course, will have to use an abstraction function that
maps the n-bit word rep in the implementation to the value type in the
spec.  This has the nice effect of moving the conversion functions that you
mention above into the abstraction function.

| Have you seen this done before in other contexts?  

This seems just like the definition of semantic domains in programming
language semantics.  

Hope I interpreted your question right and that this helps.

Regards,

--phil--


Phillip J. Windley, Asst. Professor   |  windley@cs.uidaho.edu
Laboratory for Applied Logic	      |  windley@panther.cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501  
Moscow, ID    83843                   |  Fax:   208.885.6645