[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

RE: [PVS-Help] Record subtype from a TYPE+



Cesar,

Thanks for taking a good guess.  I should have been clearer about what I'm
up to.  What I'd like to model is more like a typecast in C, or like what
happens when you encrypt data in-place in memory.  At one moment the data is
typed on a word-by-word basis.  A split second later all you should
interpret is an opaque blob of bytes (a per-word or per-byte interpretation
such as "Integer" is no longer appropriate).

Specifically, I am dealing with the contents of memory segments in general
whose type is "values," i.e. an opaque blob of data of finite but fairly
arbitrary size.  In special cases, I apply a "grid" or interpretation onto
the blob and force it to present itself as a record type.  A C typecast to a
struct is almost exactly what I'd like to accomplish.  (I hope this isn't
too vulgar for PVS...)

What I would like to say is "All memory segments contain blobs of data, but
some memory segments contain (blobs that may be correctly interpreted as)
records of type Instructions."

One case in which a solution would be helpful is as follows.  I have
currently kludged my solution using duplication:

  x,y:			VAR values
  hash( x ): Digests
  hashRepeatable: 	AXIOM	x = y		=>	hash(x) = hash(y)
  hashAvoidsCollision:	AXIOM	x /= y	=>	hash(x) /= hash(y)	

..then later, after I've defined Instructions, I repeat myself:

  i, j:			VAR Instructions
  hash( i ): Digests
  hashIRepeatable: 	AXIOM i = j		=>	hash(i) = hash(j)
  hashIAvoidsCollision: AXIOM	i /= j	=>	hash(i) /= hash(j)	

In this case, the cryptographic hash function I'm modeling is
type-insensitive.  This duplication could proliferate because there may be
many record types need to be hashed.

Thanks,

mark

-----Original Message-----
From: Cesar A. Munoz [mailto:munoz@nianet.org] 
Sent: Monday, July 17, 2006 4:36 PM
To: Mark Brown
Cc: Cesar A. Munoz; pvs-help@csl.sri.com
Subject: Re: [PVS-Help] Record subtype from a TYPE+

Mark,
Maybe this is what you are looking for:

   values : TYPE = [# a,b,c:int #]

   Instructions : TYPE+ from values


Cesar


On Fri, 2006-07-14 at 16:26, Mark Brown wrote:
> Hello,
> 
> Is there a way to have a record type also be a type FROM a supertype?  I
> want to declare that a subtype from "values" can be interpreted as a
record
> type named Instructions.  But this fails:
> 
> 	values TYPE+
> 	Instructions TYPE FROM values = [# a, b, c: int #]
> Error message:
> 	Parser error: Found '=' when expecting 'END'
> 
> Thanks,
> 
> Mark Brown
-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace        mailto:C.A.Munoz@larc.nasa.gov
100 Exploration Way, Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4