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

Re: [PVS-Help] Abtract datatypes in abstract data types



Hi Sjaak,

I tried this in PVS 5.0, and it worked without any problem - what
version are you using?

Sam

S.Smetsers@xxxxxxxx wrote:

> Hi,
> 
> Suppose I want something like:
> 
> B[A,X: TYPE] : DATATYPE
> BEGIN
> 	b_in(leftB:A, rightB:X): b_in?
> END B
> 
> DZ [A: TYPE] : CODATATYPE
> BEGIN
> 	IMPORTING B[A,DZ]
> 	dz_in(left:DZ, right:B[A,DZ]) : dz_in?
> END DZ
> 
> So actually i want DZ to be parametric in B. The above definitions are
> rejected (though the way PVS complaints about it, is a bit odd). Is  there
> a way to do this?
> 
> Thanks,
> 
> Sjaak Smetsers