 | 13.1 Introduction |
| 
| 13 SAL Translator |
| 
| 13.3 Writing transition systems and LTL assertions |
|
| 13.2 Translatable RSL constructs |
13.2 Translatable RSL constructs
Regarding V1, in the following subsections RSL constructs are
listed, showing how they are translated to SAL. More implementation details about this, can be found in [13].
Depending on the RSL kind of declaration, a declaration translates to one or more type, constant, function or variable declarations.
The RSL Scheme constructor is translated to the SAL CONTEXT constructor.
Object declarations are translated as instantiations of the SAL
CONTEXT. If the applicative specification style is used, then object instantiations only introduce a name space in the current scheme.
The Boolean, Integer, Natural, Record, Variant
and Collection types are translated. But Sort and Union types are not accepted by the translator.
Sort definitions are not accepted.
The RSL Bool type is translated to the BOOLEAN type in SAL.
As integer is infinite by definition, it is necessary to impose a
restriction over the possible values of the type. Then the translator
uses a special integer type generated automatically during the
translation as a subtype of the integer basic type of SAL (using
the subrange structure in SAL). The subtyping used is, in RSL,
of the form
|
| | | | | | | | | | | | |
| type |
| Int_ = {| x : Int • x ∈ {DefaultIntLow .. DefaultIntHigh} |}
|
The tool generates a file (IT_AN.sal) where the
Integer type definition is:
Int_: TYPE = [SAL_GLOBAL!DefaultIntLow..SAL_GLOBAL!DefaultIntHigh];
SAL_GLOBAL.sal is the name of the SAL file (also generated by the
tool) where DefaultIntLow and DefaultIntHigh are defined.
By default, they are defined as -4 and 4 respectively, but this can be
changed by the RSL specification, If a value definition of the form
is included in the specification being translated, where the type T is
Int or any subtype of Int, and n is a literal, then n will
be used as the value of DefaultIntHigh in SAL_GLOBAL.sal. A similar
definition of IntLow will cause its value to be used as the value of
DefaultIntLow.
It is necessary to make sure that DefaultIntHigh and DefaultIntLow are
set to include any integer values generated when model
checking the specification, since
- Integer arithmetic on range types in SAL is actually modulo
arithmetic, to keep within within the bounds. Hence it only models
RSL arithmetic properly when the bounds are wide enough.
- Exceeding the bounds for integers will cause errors to be
generated in the CC version.
Natural type is translated similarly to Integer type. The SAL subrange
structure is used. The subtyping is, in RSL,
of the form,
|
| | | | | | | | | | | | |
| type |
| Nat_ = {| x : Nat • x ∈ {0 .. DefaultNatHigh} }|
|
The tool generates a file (NT_AN.sal) where the
Natural type definition is:
Nat_: TYPE = [0..SAL_GLOBAL!DefaultNatHigh];
DefaultNatHigh is by default set to 4, but this value can be changed
in a similar fashion to DefaultIntHigh, by including in the
specification a value definition of the form
where the type T is
Int or any subtype of Int, and n is a literal.
Just as for integers, DefaultNatHigh needs to be large enough to
include any natural values generated during model checking.
Variants are translated to the type declarator DATATYPE in SAL. For
example, consider this example ([1], pg. 96)
|
| | | | | | | | | | | | |
| type |
| List == empty | add(head : Elem ↔ replace_head, tail : List)
|
is translated to
List: TYPE = DATATYPE
empty,
add(head: Elem, tail: List)
END;
replace_head(z_: Elem, x_: List) : List =
LET x1_ : Elem = head(x_) IN
LET x2_ : List = tail(x_) IN
add(z_ , x2_)
Note that reconstructor declarations (in this case "replace_head") are translated as explicit functions.
RSL defines records as short variant definitions. Variants in SAL are
defined with the type declarator "DATATYPE". Therefore record
definition is translated to DATATYPE in SAL.
Union type is not translatable into SAL.
The strategy for translating sets and maps relies on an encoding based
on total functions. The definition of the operations over sets and
maps use LAMBDA functions.
- Set type
The translation for sets uses an implementation based on a function
from the domain of the set into a boolean value. For example, this type declaration:
will be translated into SAL as:
Nat_set: TYPE = [NT_AN!Nat_ -> BT_AN!Bool_];
Set1: TYPE = Nat_set;
- Map type
Maps are also defined as functions but are in general not defined over
all possible values in their domains. In this case, a map application
over a value not in the map's domain will return the value swap.
SAL does not provide partial function support, so partial
constructions are not directly translatable. The translator modifies
the map by creating a variant declaration. This declaration turns the
map into a total function. For example, the following map definition
is translated to
T1_T2_map_range: TYPE = DATATYPE
T1_T2_map_nil,
T1_T2_map_range(T1_T2_map_val: T2)
END;
T1_T2_map: TYPE = [T1 -> T1_T2_map_Range];
MyMap: TYPE = T1_T2_map;
T1_set: TYPE = [T1 -> Bool_];
Non deterministic maps are not accepted in the translator. For example,
the expression
[ x ↦ y | x, y : Nat • {x,y} ⊆ {1, 2}
] cannot be translated to SAL. Infinite maps (as in [ n ↦ 2 * n | n : Nat •
is_a_prime(n) ]
) are not accepted for the translator.
- List type List definitions are not accepted.
Value definitions of the form "identifier: type
expression" (called typings) are not accepted by the translator.
Explicit value definitions are translated to a constant declarations in the model.
Implicit value definitions are not accepted by the translator.
- Explicit function definitions
Explicit function definitions are translated to SAL explicit
functions. The name of the function must be unique in the scheme. An
example of a RSL declaration is
|
| | | | | | | | | | | | |
| value |
| sum : Int × Int → Int |
| sum(x,y) ≡ x + y
|
is translated to the SAL function
sum(x:IT_AN!Int_ , y:IT_AN!Int_) : IT_AN!Int_ = x + y;
If the function name is overloaded in the specification, an error is
reported during the translation. The same happens when operators are
overloaded.
SAL does not have predefined operators over sets and maps. The
translator generates a file with macro declarations containing the names for
the set and map operations. It will be expanded before model checking
the specification. Table 13.2.1 and table 13.2.1 show function names for set operators
and map operators.
|
Operator | Function name |
|
x = y | = |
|
x ≠ y | /= |
|
x ⊃ y | strict_supset?(x, y) |
|
x ⊂ y | strict_subset?(x, y) |
|
x ⊆ y | supset?(x, y) |
|
x ⊆ y | subset?(x, y) |
|
x ∉ y | not_isin(x, y) |
|
x ∩ y | intersection(x, y) |
|
x \ y | difference(x,y) |
|
x ∪ y | union(x, y) |
|
x ∈ y | isin(x, y) |
|
|
|
Operator | Function name |
|
x = y | = |
|
x ≠ y | /= |
|
x † y | override(x, y) |
|
rng x | rng(x) |
|
x / y | restriction_to(x, y) |
|
x \ y | restriction_by(x, y) |
|
dom x | dom(x) |
|
|
- Partial function definitions
SAL does not support partial functions. The translator assumes that
all preconditions of partial functions are verified. The tool, in V1, translates partial functions
as SAL total functions. For example,
|
| | | | | | | | | | | | |
| value |
| diff : Nat × Nat -~-> Nat |
| diff(x,y) ≡ x - y |
| pre x ≥ y
|
is translated to
diff(x:NT_!Nat_ , y:NT_!Nat_): NT_!Nat_ = x - y;
- Recursive function definitions As in SAL, recursive function definitions are not accepted by the translator.
- Implicit function definitions Implicit function definitions
are not accepted by the translator.
Variable declarations are not
accepted by the translator.
Channel declarations are not
accepted by the translator.
Axiom declarations are not
accepted by the translator.
Test case declarations are
ignored by the translator.
The translation of a class expression results in the translation of
its declarations and its statements.
Extending class
expressions are translated as a new class declarations. An
extending class expression includes all the extended class declarations.
Hiding class expressions
are ignored by the translator.
Renaming class expressions
are ignored by the translator.
With expressions
are ignored by the translator.
The translator only works with
specifications written in an applicative style. So, the role of
schemes is to provide type and value
declarations.
An object expression which is an "object name" is accepted as a
qualification. The following example, shows how
object expressions are translated.
|
| | | | | | | | | | | | |
| object N : NAMES |
| value |
| f : N.Name → Bool |
| f(n) ≡ N.to_bool(n)
|
is translated to
f(n: SAL\_TYPES!Name) : Bool_ = NAMES!to_bool(n);
Neither object array expressions nor fitting object expression are accepted by the translator.
RSL's basic type system uses the SAL type system for translating RSL
type expressions.
Type names translate to type names.
Product type expressions translate to SAL tuple declarations. For
example,
MyProd = Nat × Bool × Int
is translated to
Prod : TYPE = [NT_AN!Nat_ , BT_AN!Bool_ , IT_AN!Int_];
The translator generates a new set context for every
set declaration/type expression found. Multiple set declarations of the same domain type
are avoided. Set type expressions like,
MySet = (Nat × Int)-set
are rejected by the translator.
Only sets in which the
domain is either a basic type or a defined type are accepted. So the expression in
the previous example must be
changed into:
MyData = Nat × Int,
MySet = MyData-set
List type expressions are not accepted by the translator.
As in set type expressions, the translator generates a new finite map
context for every map declaration/type expression found. Multiple map
declarations of the same domain type are avoided.
Neither infinite maps nor non-deterministic map type expressions are
allowed by the translator.
In general, the way to translate function type expressions is shown in
13.2.1. However, there are some exceptions:
- Curried functions are transformed into lambda functions.
- Function-type declared values are declared as function
type and the value expression (a lambda abstraction expression)
is assigned to it. For example,
|
| | | | | | | | | | | | |
| value |
| sum: Int × Int → Int = λ (x,y) : Int × Int • x+y
|
is translated to
sum :[ [IT_AN!Int_, IT_AN!Int_] -> IT_AN!Int_ ] =
LAMBDA (x:IT_AN!Int_, y:IT_AN!Int_): x + y;
Subtype expressions are translated to SAL subtype declarations. For
example, the following subtype expression,
T = { | (x,y): Int × Int • x > y
| }
is translated to
T: TYPE = {TypeId1_ :[IT_AN!Int_, IT_AN!Int_] | TypeId1_.1 >
TypeId1_.2};
There are four special case for Int and Nat:
T1 = { | x: Int • x ∈
{a..b} | }
is translated to
T1: TYPE = [a..b]
T2 = { | x: Nat • x ∈
{a..b} | }
is translated to
T2: TYPE = [a..b]
- T3 = { | x: Nat • x <= a
| }
is translated to
T3: TYPE = [0..a];
- T4 = { | x: Nat • x < a
| }
is translated to
T4: TYPE = [0..a-1];
A bracketed type expression translates as its constituent type expression.
Value expressions are translated of different forms.
The RSL value literals Bool, Int and Nat are
translated but Unit, Real, Char and Text are not accepted by the translator.
A name translates as a name.
Pre names are not accepted by the translator.
The RSL basic expression skip is ignored and stop, chaos and swap are not accepted in the translator.
A product expression
translates to a SAL tuple.
All set expressions are accepted
by the translator. Set expressions are modelled as total
functions. They return true when they are applied to a member
of the set, and false otherwise. The table 13.2.5, shows
as set expressions are
translated to SAL. The
context name “SET_OPS” is used only for illustrative purposes.
|
RSL | SAL |
|
{} | SET_OPS!emptySet |
|
{x, y} | SET_OPS!add(x, SET_OPS!add(y, SET_OPS!emptySet)) |
|
{x .. y} | LAMBDA (z :IT_AN!Int_): x <= z AND z <= y |
|
{ b | b : T • p(b) } | LAMBDA (b :T): p(b) |
|
{ f(b) | b : T • p(b) } | LAMBDA (u :U): EXISTS (b :T) : p(b) AND f(b) = u |
|
|
|
RSL | SAL |
|
[ ] | MAP_OPS!emptyMap |
|
[ x ↦ p, y ↦ q ] | MAP_OPS!add(x,p,MAP_OPS!add(y,q,MAP_OPS!emptyMap)) |
|
[ b ↦ e | b : T . p ] | LAMBDA (b :T): IF p THEN m(e)=b ELSE nil ENDIF |
|
|
[ e1(x) ↦ e2(x) | x : T . p(x) ]
(where e1 : T → U1, e2 : T → U2),
are not accepted by the translator (because there is no way, in general, to generate the inverse function of “e1”).
List application
expressions are not accepted by the translator.
Function expressions are
translated to SAL's LAMBDA abstraction.
An application
expression is translated to a function call or a map
application. List applications are not accepted by the translator.
All quantified
expressions are accepted. Regarding the translation mechanism,
except exist !, all
quantifiers are directly supported by SAL. The translation of
the ∃! expression is described following,
EXISTS (x:T) : p(x) AND ( FORALL (x1:T) : p(x1) => x = x1 )
Equivalence expressions
are translated to SAL equalities.
Post expressions are not
accepted by the translator.
Disambiguation
expressions are ignored (except set or map expressions which
involve empty sets or empty maps).
Bracketed expressions
are translated to SAL bracketed expressions.
Statement infix expressions
are not accepted by the translator. On the other hand,
the translation of the axiom infix expressions is
straightforward. Table 13.2.5 shows how infix operators
are translated.
|
RSL | SAL |
|
⇒ | => |
|
/\ | AND |
|
\/ | OR |
|
|
Equality/Inequality infix operations for set and map, remain as
infix operations in the translated code (collections are
implemented as functions).
The names of the operations showed in tables 13.2.1
and 13.2.1, are turned into prefix operations during the
translation process (SAL does not support
infix operator definitions for them).
A prefix expression
generally translates to the corresponding SAL expression.
For example, the expression ~ translates to NOT. The universal prefix expression, □, is not
accepted by the translator.
The rest of the value prefix expressions translate to a
function calls, using the function names described in Table 13.2.5.
On the other hand, the prefix operators int, real, card, len, inds, elems, hd and tl are
not accepted by the translator.
|
RSL | SAL |
|
abs | abs |
|
dom | dom |
|
rng | rng |
|
|
let x = 0 in x + 1 end
is translated to
LET x : IT_AN!Int = 0 IN x + 1;
Also it is possible translate more complex expressions, as you can see
in the next example,
|
| | | | | | | | | | | | |
| type |
| Prod = Int × Int |
| value |
| cons : Int × Int → Prod |
| cons(a, b) ≡ let res = (a,b) in res end
|
is translated to
Prod: TYPE = [IT_AN!Int_, IT_AN!Int_];
cons(a :IT_AN!Int_, b :IT_AN!Int_) : SAL_TYPES!Prod =
LET res :[IT_AN!Int_, IT_AN!Int_] = (a, b) IN res;
The type of the bounded name in the let definition must be explicitly
stated in SAL’s model. On the other hand, the translation of binding involving products is more complex than
previous cases. SAL imposes that there is only single binding in
let expressions, preventing let expressions of the form "let (a,b) = P in" (where P is of product type).
However, in SAL, product fields can be accessed by an index
associated according the field position inside the
product. The tool uses this feature to translate these expressions to
SAL. For example,
|
| | | | | | | | | | | | |
| value |
| test : Prod → Bool |
| test(p) ≡ let (a,b) = p in a > 1 end
|
is translated to
test(p :SAL_TYPES!Prod): BT_AN!Bool_ =
LET LetId3_ : SAL_TYPES!Prod = p IN LetId3_.1 > 1;
The if expression translation is straightforward because SAL provides
IF-THEN-ELSE and ELSIF constructions. For example, the following
expression ([1], pg. 21)
if x > y then x - y else y - x end
is translated to
IF x > y THEN x - y ELSE y - x ENDIF
A case expression is translated as a nested sequence of "if"
expressions. For example, the expression
|
| | | | | | | | | | | | |
| case x of |
| 1 → 10, |
| 2 → 20, |
| _ → 0 |
| end
|
is translated to
IF (x = 1) THEN 10
ELSIF (x = 2) THEN 20
ELSE 0
ENDIF
Iterative expressions
while, until and for are not
accepted by the translator.
Chris George, April 17, 2008
| 13.2 Translatable RSL constructs |
| 13.1 Introduction |
| |
| 13 SAL Translator |
| |
| 13.3 Writing transition systems and LTL assertions |
|