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

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