[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [PVS-Help] Abtract datatypes in abstract data types
I tried this in PVS 5.0, and it worked without any problem - what
version are you using?
> Suppose I want something like:
> B[A,X: TYPE] : DATATYPE
> b_in(leftB:A, rightB:X): b_in?
> END B
> DZ [A: TYPE] : CODATATYPE
> 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?
> Sjaak Smetsers