11.2 Activating the PVS translator	11 PVS translator	11.4 Class expressions
11.3 Declarations

11.3 Declarations

Note that PVS has a define before use rule. This means that the order of type and value declarations in PVS may differ from that in RSL.

11.3.1 Scheme declarations

There is an exception to this for non-parameterized schemes used in class scope expressions, as we see in section 11.7.29.

11.3.2 Object declarations

Theories in PVS cannot be nested. So nested object declarations are "flattened". For example, consider the following RSL scheme definition:

This translates to:

This means that we do not accept object classes that reference entities in their context. For example a_body cannot refer to anything in s_body.

An object definition with a formal array parameter is not accepted: object arrays are normally only used in imperative or concurrent specifications.

11.3.3 Type declarations

Type declarations are translated according to their constituent definitions.

Mutually recursive type definitions are not accepted.

Sort definitions

Sort definitions are translated into uninterpreted type definitions in PVS.

However PVS distinguishes between empty (defined with the reserved word TYPE) and nonempty types (defined with the reserved word TYPE+). This syntactic distinction does not exist in RSL and can be important in the transformation since the PVS type checker will generate an existence TCC for every function declared if it can not determine if the result type of the function is a nonempty type. This is so since PVS considers inconsistent the existence of a function with possibly empty result type. (In RSL such a function with parameters from non-empty types would be evidence of the non-emptiness of the result type.)

So we translate every RSL sort into a PVS nonempty type (TYPE+). But this extends somewhat the transformation since it is like adding in RSL:

axiom ∃ t: T • true

This is unlikely to cause any problems in extending the RSL theory since the declaration of a value of type T or a total function with non-empty domain type and result type T would also imply it. Since it avoids getting extra TCCs we adopt it.

Variant definitions

Variant types in RSL translate directly into PVS DATATYPEs.

PVS DATATYPEs are very similar to RSL variant types, except that:

• PVS includes recognizers, boolean functions that return true if their argument is in the corresponding variant. These are added to the translation, given names formed by appending "?" to the constructor name.

• All components in PVS need accessors corresponding to RSL's destructors. In RSL these are optional: the translator generates missing ones with names of the form acc_n_, where n is an integer used to make unique names, and warns the user that they have been generated.

• PVS does not include RSL's optional reconstructors, so when these are included they are added by defining them explicitly as functions in PVS.

• RSL allows wildcard constructors. These are not accepted by the translator.

For example, the following RSL variant type definition:

generates the following PVS definitions:

  V: DATATYPE
  BEGIN
    Vconst: Vconst?
    Vint(acc_1_: int): Vint?
    Vrec(d1Vrec: int, d2Vrec: V): Vrec?
  END V

  r1Vrec(z_: int, x_: {x_: V | Vrec?(x_)}): V = 
    LET x1_ = d1Vrec(x_), x2_ = d2Vrec(x_)
    IN Vrec(z_, x2_);

Short record definitions

Abbreviation definitions

Union Definitions

11.3.4 Value declarations

Typings

Explicit value definitions

Implicit value definitions

Explicit function definitions

If the function has a precondition this is translated into a subtype for the last parameter. For example, the RSL definition

translates to

  diff(x: nat, y: {y: nat | x >= y}): nat = x - y;

Access descriptors are not accepted. The kind of function arrow (→ or -~->) does not matter.

It is not required that the number of parameters matches the number of components in the domain of the function's type expression. For example, the following are all accepted:

Recursive functions need MEASUREs in PVS to show that they terminate. Generating measures automatically is not possible in general, so the translation is to a constant declaration giving the function signature plus an axiom defining the function body. Preconditions are dealt with as for non-recursive functions.

Implicit function definitions

11.3.5 Variable declarations

11.3.6 Channel declarations

11.3.7 Axiom declarations

11.3 Declarations
11.2 Activating the PVS translator	11 PVS translator	11.4 Class expressions