 | 11.1 Introduction |
| 11 PVS translator |
| 11.3 Declarations |
|
|
| ||||||
| 11.2 Activating the PVS translator | ||||||||
rsltc -pvs <file>
where <file> takes the form X or X.rsl and
contains the RSL scheme, object, theory or development relation named
X. It generates a file X.pvs, plus perhaps other
PVS files generated from RSL files in the context of X. For each such
file Y.rsl, any corresponding pvs file will be called Y.pvs.
X.pvs can be loaded into pvs using the shell command
pvs X.pvs
provided the current directory is that where X.pvs is stored.
PVS sets up a PVS context in each directory where it is used on PVS files. Such a PVS context needs also to load a file rsl_prelude.pvs. This RSL prelude is a library of definitions in PVS that are used by the translator, plus some theorems that may be used in proofs.
Before loading the RSL prelude for the first time you need to run PVS on it to set up some auxiliary files. All you need to do is start PVS in the directory where rsl_prelude.pvs is stored, use the command
load-prelude-library <pvs_path>/lib/finite_sets
where <pvs_path> is the directory where PVS is stored, to load the PVS finite sets library, load the file rsl_prelude.pvs, run the PVS type checker, and exit.
You only need to do this once, unless you move to a new version of PVS, when you might have to do it again to update the auxiliary files.
When you create a context for a directory in which you wish to store PVS files generated from RSL ones, you need to load the RSL prelude. You do this with the PVS command
load-prelude-library <path>
where <path> is the path of the directory where rsl_prelude.pvs is stored. You only need to do this once for each context. In PVS you issue a command using the Meta key (usually Esc) followed by x, and then typing the command in the minibuffer.
The RSL prelude is a natural place to add theorems about RSL that you find useful. You can do this by adding such theorems to rsl_prelude.pvs, but a perhaps better way is to create your own prelude file in the same directory. You could use the translator to generate the file from RSL. Since libraries are loaded by directory rather than file, your file will be loaded automatically in PVS contexts in which you have issued the load-prelude-library command. We would be interested to receive such extensions -- with their proofs! -- and perhaps include them in the RSL prelude in later releases.
Correctness is important for any translator, but particularly so when the idea is to enable proofs of properties of the translated specification. Correctness is defined in terms of soundness: an RSL specification is correctly translated if the translation is sound, which means that no theorem can be proved in PVS which is not valid for the RSL specification. We would also like the translation to be complete, i.e. we would like all true theorems to be provable. This is not easy to show -- it depends on the power of PVS as well as on the translation -- but we try to achieve it, and know of no exceptions.
There are two levels at which we consider correctness. Most of the RSL types and type constructors map directly into corresponding PVS types and type constructors. It is then a fairly routine task to map most of the RSL value functions, operators and constructors onto PVS ones, adding to the basic PVS theory when necessary.
But there is a deeper question of the adequacy of PVS to represent all RSL types and values. If, for example, the mapping is not injective then we will effectively equate different RSL values by mapping them to the same PVS ones, and the translation would not be sound: we would effectively create theorems that do not necessarily hold in PVS.
Concurrency and imperative constructs have no counterpart in PVS, so we exclude them from the translation. More problematic is the RSL logic, which permits potentially undefined and nondeterministic expressions. We cannot represent these by PVS expressions, so we have to exclude them. Some like the basic expressions chaos and swap can be excluded syntactically. The internal choice operator is also excluded syntactically. Nondeterminism in maps can be handled by either making sure that the translated RSL will generate suitable TCCs for the PVS, or by generating the required conditions as extra PVS LEMMAs. No proof in PVS can be considered sound unless the TCCs and all lemmas are proved. Generation of swap in applicative specifications can be checked by confidence conditions for the completeness of case expressions and possible matches in some let expressions.
There remain two issues which we cannot easily handle completely formally, where the RSL theory of the specification is effectively strengthened by the translated PVS theory: recursive functions and nondeterministic let expressions. We can summarize this by noting that in PVS the equality e = e holds for any expression e. In RSL this is not true if e is undefined or is nondeterministic, and this will occur if e is a non-terminating application of a recursive function, and may occur if e involves an implicit let expression (or, equivalently, the application of hd to a set or map). So users should be aware that these must be checked by them. Recursive functions should be terminating, and any use of nondeterminism should involve only weak nondeterminism: i.e. the value of any function using nondeterminism should not itself be nondeterministic.
A translation should therefore only be considered correct if:
We expect the second condition to hold, but the translator does not check, for example, that no identifier is used which clashes with a reserved word in PVS (see section 11.10), or that the "flattening" of object declarations causes no scope errors (see section 11.3.2).
| 11.2 Activating the PVS translator | ||||||||
|
|
| ||||||