 | 11.6 Type expressions |
| 11 PVS translator |
| 11.8 Bindings and typings |
|
|
| ||||||
| 11.7 Value expressions | ||||||||
The RSL value literals are translated into their PVS counterparts.
There are no real literals in PVS, so a real literal i.d (where i is the integer part of the real number and d its decimal part) is translated into i + d/10dn where dn is the number of decimal digits.
A value name translates as a name.
Not accepted.
Basic expressions (chaos, skip, stop, and swap) are not accepted.
A product expression translates to a PVS tuple expression.
Sets are modelled in the PVS prelude as functions that return true when applied to a member of the set, false otherwise.
All set expressions are accepted, as illustrated below.
| RSL | PVS |
| {} | emptyset |
| {x, y} | add(x, add(y, empyset)) |
| {x .. y} | LAMBDA (z : int): x <= z AND z <= y |
| { b | b : T • p } | { b : T | p } |
| { e | b : T • p } | { u : U | EXISTS (b : T) : p AND u = e} |
The third example is a special case of a set comprehension. The more general case is the last, where u is a new identifier not free in p or e, and U is the type of e.
All finite list expressions are accepted, as illustrated below.
| RSL | PVS |
| ⟨⟩ | (::) |
| ⟨x, y⟩ | (:x, y:) |
| ⟨x .. y⟩ | ranged_list(x, y) |
| ⟨e | b in l • p⟩ | map(LAMBDA (b: {b: T | member(b, l) AND p}): e, |
| filter(l, LAMBDA (b: {b: T | member(b, l)}): p)) | |
All map expressions are accepted, but either RSL confidence conditions or PVS TCCs may be generated to check the map is deterministic. Examples are shown below.
| RSL | PVS |
| [] | emptymap |
| [x ↦ p, y ↦ q] | add_in_map(x,p,add_in_map(y,q,emptymap)) |
| [b ↦ e | b : T • p] | LAMBDA (b : T): IF p THEN mk_rng(e) ELSE nil ENDIF |
| [e1 ↦ e2 | b : T • p] | LAMBDA (u : U): |
| LET b = RSL_inverse(LAMBDA (b : T): e1)(u) IN | |
| IF p THEN mk_rng(e2) ELSE nil ENDIF | |
same as the PVS prelude's inverse function, but with a subtype to generate a TCC that LAMBDA (b : T): e1 is an injective function, a sufficient condition for the map to be deterministic. u is a new identifier not free in p, e1, or e2, and U is the type of e1.
A confidence condition that x≠y is generated for the second example, again a sufficient condition for the map to be deterministic.
Function expressions are accepted.
An application expression may be translated to a function call, a list application or a map application.
Quantified expressions are accepted.
Equivalence expressions translate as equalities in PVS.
Post expressions translate as LET expressions, as shown below.
Disambiguation expressions are accepted.
A bracketed expression translates to a bracketed expression.
An infix expression translates to the corresponding PVS expression. Some infix operators in RSL translate to functions in PVS.
A prefix expression translates to the corresponding PVS expression.
The universal prefix expression □ e is translated as e, since □ e is equivalent to e for applicative expressions.
Not accepted.
Not accepted.
Not accepted.
Not accepted.
Not accepted.
Let expressions are accepted.
If expressions are accepted.
Case expressions are accepted. They translate to PVS IF expressions since the case patterns in RSL are more general than those in PVS.
Not accepted.
Not accepted.
Not accepted.
A class scope expression translates to a PVS THEORY. So an RSL theory containing several class scope expressions as axioms will in general translate to a PVS file containing a number of theories. The PVS THEORY from the class scope expression in C ⊦ p contains the translation of the class expression C plus the translation of p as a LEMMA, i.e. something to be proved.
When, however, a number of class scope expressions have a class expression which is an instantiation of the same non-parameterized scheme, the scheme is translated as a separate PVS THEORY and the class scope expressions are translated as a single THEORY that imports the THEORY for the scheme and contains all the resulting LEMMAs. This makes it possible to use earlier lemmas in proving later ones, since they share the same definitions from the imported THEORY.
These are expanded into their conditions and these conditions translated.
| 11.7 Value expressions | ||||||||
|
|
| ||||||