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

[PVS-Help] Theory interpretations

I have recently attempted to use theory interpretations to instantiate 
the base of a sequence of theories that define a particular 
specification type. I have two uninterpreted types in a theory:

data_id: TYPE
data_value: TYPE

and then an interpreted type:

data_state: [data_id -> data_value]

I would like to override these all to give me:

example_data_id: TYPE = {...}
example_data_value: TYPE = {...}
example_data_state: TYPE = [new_data_id -> new_data_value]

I am not sure if the last function can be overridden in a reasonable way 
through interpretations, so if that won't work, the rest of this 
question is moot.

I run into problems because of the structure of my import chain. There 
are essentially two parallel import chains:

an abstract specification import chain
state -> module -> application -> system specification and

an example instantiation import chain
example_state (IMPORTING state) -> example_module (IMPORTING module) -> 
example_application (IMPORTING application) ...

where the uninterpred types above are part of state and every theory 
except state defines records, and so I am not trying to fill the others 
out with interpretations, but rather am filling in values for the 
various record fields.

I can get the example_state theory to work OK, but when I try to create 
the example_application theory, for instance, I instantiate a record 
field that is defined through the state theory to be of type data_id but 
for which I would like to supply an example_data_id. If I do this, I get 
a typecheck error.

Is there a way to do what I want?

Many thanks,