[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
IMPORTING in PVS
Hello all,
I am using PVS as the guts of a new specification language in the
spirit of "structural embeddings". I have a nice correspondence between
modules in the specification language and PVS theories, but I am having
some problems with scoping in PVS.
For an entity in the specification language, say class C defined as
class C is i : integer; end;
I generate the declarations
C : TYPE+
i : [C -> int]
in two different PVS theories T1 and T2. Additionally, T1 may include
theorems that talk about C and i.
When I use the theories, I import both of them in T3. The problem now is
that C and i are ambiguous in T3. The only things of interest in T1
are the theorems, and I tried to export only them. To this PVS complains
that I must export C and i as well.
Is it possible to indicate that in T3, C and i refer to T2.C and T2.i?
I guess I am after a "qualified import" feature of some programming
languages.
I could of course fully qualify all names, but the result is not really
aesthetically pleasing.
--
pertti