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

[PVS-Help] Abtract datatypes in abstract data types



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