Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <9212111938.AA02293@ultrastar.EE.CORNELL.EDU>
From: markaa@EDU.CORNELL.EE.ultrastar (Mark D. Aagaard)
Date: Fri, 11 Dec 1992 14:38:12 -0500
Organization: Cornell University, Electrical Engineering, Ithaca NY 14853
To: info-hol@edu.uidaho.cs.ted
Subject: representing numbers

Tim and Phil -

Your conversation triggered some thoughts that I have been toying with.
I don't have any solutions, but here is the way that I would phrase
the problem:

In hardware, different modules interpret data words differently.
For example: memory presumably wants to treat all words the same, 
but the integer unit wants to treat words as bounded integers, 
the floating point unit wants to treat words as bounded reals with 
finite precision, the instruction unit wants to treat words as 
opcodes and operands, etc etc. 

Also, within a single module, one would probably want to
treat a word at different levels of abstraction. For example, with
floating point numbers: at one level a floating point value is a
a real number; at another level it is a tuple consisting of a
single bit for the sign, some number of bits for the mantissa and
some number of bits for the exponent; somewhere in between these two
levels a floating point value can be treated as a sign, an integer
for the mantissa and an integer for the exponent. 

At any point in time the underlying representation for a word should
remain hidden from the user, which would mean using abstract datatypes.
So, there will need to be conversion functions for going between different 
levels of abstraction and between different interpretations. 

The goal would be to provide a mechanism which efficiently supports these 
different interpretations and abstractions. By "efficiently" I mean that
specifications and proofs should not become cluttered with extraneous
conversions and automated support should be provided to reason about 
the different interpretations and abstractions.

 -mark aagaard
  markaa@ee.cornell.edu