11.5 Object expressions11.5 Object expressions
11 PVS translator 11 PVS translator
11.7 Value expressions 11.7 Value expressions
11.6 Type expressions

11.6 Type expressions

11.6.1 Type literals

Except for Unit the RSL type literals are translated into the corresponding PVS types as shown below.

RSL PVS
Bool bool
Int int
Nat nat
Real real
Char char
Text string
Type literals
 

The only possible problem is that in PVS int is a subtype of real, while the corresponding RSL types are different. This means we must be careful with division and exponentiation, to make sure they give integers with integer arguments.

11.6.2 Names

A type name translates to a type name.

11.6.3 Product type expressions

A product type expression translates to a PVS tuple type.

11.6.4 Set type expressions

Both finite and infinite set type expressions translate to the PVS type set. It would be possible to use finite_set for finite sets, but in practice this generates a TCC for every function returning such a value, which is tedious to prove. Only the card operator actually requires a set to be finite, so it is better to prove finiteness only when it is required.

11.6.5 List type expressions

A finite list type expression translates to the PVS type list.

Infinite lists are not accepted.

11.6.6 Map type expressions

Finite and infinite maps are translated into a PVS type map defined in the RSL prelude.

The translation of a map is as a function from the domain type to a DATATYPE:

Maprange[rng: TYPE]: DATATYPE
  BEGIN
    nil: nil?
    mk_rng(rng_part: rng): nonnil?
  END Maprange

The result type nil when a map is applied indicates the argument is not in the domain. The RSL map application expression m(d) translates to rng_part(m(d)), which will generate the appropriate TCC nonnil?(m(d)) expressing that d is in the range of m.

The map type does not include nondeterministic maps: these are not accepted.

11.6.7 Function type expressions

A function type expression translates to PVS function type.

PVS functions are total. We partly deal with partiality in RSL functions: preconditions generate subtypes as described earlier for the translation of functions (section 11.3.4), but nondeterminism is not accepted.

Access descriptors are not accepted.

11.6.8 Subtype expressions

A subtype expression translates to a PVS subtype.

11.6.9 Bracketed type expressions

A bracketed type expression translates as a PVS tuple type with one member.

Chris George, March 3, 2005

11.6 Type expressions
11.5 Object expressions11.5 Object expressions
11 PVS translator 11 PVS translator
11.7 Value expressions 11.7 Value expressions