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


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

I could of course fully qualify all names, but the result is not really
aesthetically pleasing.