11 PVS translator	11.2 Activating the PVS translator
11.1 Introduction

11.1 Introduction

The PVS translator was written by Aristides Dasso, as reported in [7].

The subset of RSL that is accepted by the translator is the applicative subset of RSL: it excludes variables, channels, and the sequential and concurrent combinators. It also excludes union types and object arrays.

11.1.1 Use

There are two main reasons for using the PVS translator:

1. To prove RSL confidence conditions.

2. To prove RSL theories and development relations

Confidence conditions

Most confidence conditions appear as PVS type correctness conditions (TCCs) and so need not be generated by the translator. But a few will not become TCCs, and are generated as LEMMAs (with names ending _ccn, where n is a number). So if you prove all the PVS TCCs and all such lemmas, you will have proved all the confidence conditions.

The confidence conditions that translate to PVS LEMMAs are:

• Enumerated maps have distinct domain elements.

• Explicit recursive functions return values in the result type, if this is a subtype.

• Case expressions are complete.

• Let patterns can be matched.

Theories and development relations

Theories and development relations translate into PVS LEMMAs, and so are proved by proving the lemmas in PVS

11.1.2 Compilers and platforms

The translator is intended for use with PVS, available from http://pvs.csl.sri.com/. It will work with version 2.4 and above of PVS. PVS is currently only available for Solaris and Linux. It can be used free for non-commercial purposes.

11.1.3 Known errors and problems

There are no known errors.

Correctness of the translation is dependent on some conditions being fulfilled, which are generated either as type correctness conditions (TCCs) by PVS when it is run, or as lemmas corresponding to some RSL confidence conditions. See the discussion in section 11.2.3.

During translation, error messages may be generated with the standard file:line:column format showing from where in the RSL specification the message was generated. The cause of the error must be corrected and the translator run again.

11.1 Introduction
	11 PVS translator	11.2 Activating the PVS translator