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

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



Mark,
What you may need is not a subtype but a CONVERSION, which behaves
exactly as a type casting.

You could define an abstract type 
Data : TYPE+

and "concrete" types: 

Value          : TYPE+ 
Instructions : TYPE+ 

Now, you define 

Value2Data(v:Value): Data

Inst2Data(i:Instructions) : Data

But, you don't want to convert all the time from Value/Instructions to
Data. Therefore, you declare them as CONVERSIONS:

   CONVERSION Value2Data
   CONVERSION Inst2Data

PVS will automatically convert any Value into a Data and any Instruction
into a Data when needed. 

Then, you declare your axioms on Data

  x,y : VAR Data 

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


Finally, because the conversions, you can apply hash indistinctively to
values or instructions:

  v : Value
  i,j : Instructions

  foo : LEMMA 
    hash(i) = hash(v) 

Of course, you may need a few more axioms for Value2Data and Inst2Data,
e.g., bijection, if you want to prove that hash(i) = hash(j) IMPLIES i =
j.

Cesar 



On Mon, 2006-07-17 at 21:53, Mark Brown wrote:
> 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