 | 11.6 Type expressions |
| 
| 11 PVS translator |
| 
| 11.8 Bindings and typings |
|
| 11.7 Value expressions |
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} |
|
|
Set expressions
|
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)) |
|
|
List expressions
|
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 |
|
|
Map expressions
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.
|
RSL | PVS |
|
e as b post p | LET b = e IN p |
|
|
post expressions
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.
Chris George, April 17, 2008
| 11.7 Value expressions |
| 11.6 Type expressions |
| |
| 11 PVS translator |
| |
| 11.8 Bindings and typings |
|