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

[PVS-Help] adt_union



dear pvs-help:
are there any ways to union arbitrary two ADT into one ADT?
i.e.
if i hava
adt_1 : datatype
a: a?
b: b?
d(n:nat):d?
end adt_1

and

adt_2 : datatype
a: a?
e: e?
d(n:nat):d?
end adt_2

can i get a super ADT adt_union for union adt_1 andt adt_2,it should be
the form:

adt_union datatype
a: a?
b: b?
e: e?
d(n:nat): d?
end adt_union

and if a variable a of type of adt_union is given, i can decide it is a
member of adt_1, or adt_2 or both?


thanks in advance.

2005/06/08 Q. G XU