System of inference rules for RSL translation

In the following system of inference rules, the translation from RSL to the intermediate language is defined by the operator.

Contexts

When translating an RSL specification to the intermediate language, it is often the case the translation result from a declaration is used in multiple parts of the intermediate language.

An example of this is the transition system declaration. This declaration con-tains information relevant for both the symbol table, initial value and transition relation part of the intermediate language.

Because of this, the concept of contexts has been introduced in the following system of inference rules. Then by using four different context keyword and applying them to the appropriate rules, it is possible to produce the desired

output based on which part of the intermediate language is being created. The following context keywords are used:

st : symbol table iv : initial values tr : transition relation ps : property specifications

Contexts are placed to the left of the symbol `. So c ` ee⁰ means that e translates to e’ in context c. Some RSL constructions only contribute to the translation in a given context. An example of this could be a type declaration, which only contributes in the context ’st’ (when defining the symbol table).

This is reflected by adding a rule such as the following, where represents the empty translation result:

c6=st c`type_decl

Because many of the RSL constructs should be translated the same regardless of the context (e.g. operators), the context notation is only used for rules where is makes a difference for the translation. Such rules are simply denoted without using context, as such:

ee⁰

This means thate translates toe’ regardless of the given context.

Besides the contexts mentioned earlier, the context ’vs’ is also used, but for another purpose. When translating transition rules, the variables which are not updated by the rule must be part of the translation. Therefore, the context ’vs’

is used to collect the identifiers of all variable definitions. The context can then be passed on to the inference rule for transition rules, where it is compared with the set of variables that are updated in the transition rule.

Term variables

In order to make the rules more concise, some term variables will be used throughout the system of inference rules. These term variables only matches constructs in to the subset of RSL defined in Section4.1.

s : Any string, typically an identifier.

e : A value literal or an identifier, i.e. the smallest component of any value expression.

op : An operator.

ve : A value expression, meaning any combination of literals, identifiers, op-erators, if expressions or case expressions. The term e is also a value expression.

be : A boolean expression, i.e. a value expression that evaluates to a boolean value.

type : A type name.

List notation

Also note, that a shorthand notation ’..’ is used whenever a construction contains an unknown number of terms. For instance, a variant definition may contain any number enumerators, and is therefore represented as the following:

type==e₁|..|e_n

When using the translation operator with this notation, it corresponds to translating each of the elements separately. This way, the following two con-structions are equivalent whenn= 4:

e1e⁰₁, e2e⁰₂, e3e⁰₃, e4e⁰₄ e₁|e₂|e₃|e₄ e⁰₁|e⁰₂|e⁰₃|e⁰₄

e₁, .. , e_ne⁰₁, .. , e⁰_n e1|..|en e⁰₁|..|e⁰_n

Normal form

As described in Sections4.3.3and 4.3.4, value expressions containing if or case expression are rewritten such that case expressions become if expressions, and if expressions become the outermost construction.

Value expression that adhere to these requirements is said to be innormal form.

A value expression in normal form must adhere to the following rules:

• The value expression does not contain case expressions.

• The value expression does not contain if expression with elsif branches.

• The value expression does not contain if expression as part of an infix, prefix or function application expression.

This concept of normal form is used in some of the following inference rules, to determine whether further rewriting of a value expression is necessary.

Here are some examples of value expressionnot in normal form:

x=1+if true then2else 3end

x=ify=1then1else2 end+ify=2then3else 4end

Here are the same expression rewritten to normal form:

if true thenx=1+2else x=1 +3 end ify=1∧y=2thenx=1 +3else

ify=1 ∧ ∼(y=2)thenx=1+4else

if∼(x=1)∧y=2thenx=2 +3 elsex=2+4 end

end end

An example of rewriting value expressions using the system of inference rules can be found in AppendixA.2.

4.3.5.1 Scheme declarations

The following inference rules define the translation operator for scheme dec-larations:

st`schemesym_tab_def s, vs iv`schemeinit_vals

tr, vs`schemetrans_rel ps`schemeprop_specs

scheme sym_tab_def s init_vals trans_rel prop_specs

(4.1)

wherescheme is a scheme declaration

st`decl1, .. , declndecl⁰₁, vs1, .. , decl⁰_n, vsn

st`schemes= class

decl1

..

decln

end

SY M_T ABLE_DECL decl⁰₁.. decl⁰_n

SY M_T ABLE_DECL_EN D, vs1∪..∪vsn

(4.2)

wheredecli is a type declaration, value declaration, transition system declaration or LTL assertion declaration

iv`decl<sub>1</sub>, .. , decl<sub>n</sub>decl<sup>0</sup><sub>1</sub>, .. , decl<sup>0</sup><sub>n</sub> iv`schemes=

class decl1

..

decln

end

IN IT_V ALS decl₁⁰ .. decl_n⁰

IN IT_V ALS_EN D

(4.3)

wheredecl_i is a type declaration, value declaration, transition system declaration or LTL assertion declaration

tr, vs`decl1, .. , declndecl<sup>0</sup><sub>1</sub>, .. , decl<sup>0</sup><sub>n</sub> tr, vs`schemes=

class decl1

..

decln

end

T RAN S_REL decl⁰₁.. decl⁰_n

T RAN S_REL_EN D

(4.4)

wheredecliis a type declaration, value declaration, transition system declaration or LTL assertion declaration

ps`decl<sub>1</sub>, .. , decl<sub>n</sub>decl<sup>0</sup><sub>1</sub>, .. , decl<sup>0</sup><sub>n</sub> ps`schemes=

class decl1

..

decln

end

P ROP_SP EC decl₁⁰ .. decl⁰_n

P ROP_SP EC_EN D

(4.5)

wheredecl_iis a type declaration, value declaration, transition system declaration or LTL assertion declaration

4.3.5.2 Type declarations

The following inference rules define the translation operator for type decla-rations:

type_def₁, .. , type_def_ntype_def₁⁰, .. , type_def_n⁰ st`type

type_def1, ..

type_def_n

type_def₁⁰ .. type_def_n⁰, {}

(4.6)

wheretype_defi is an abbreviation type definition or a variant type definition

c6=st

c`type_decl (4.7)

wheretype_decl is a type declaration

4.3.5.3 Value declarations

The following inference rules define the translation operatorfor value decla-rations:

value_def1, .. , value_defnvalue_def₁⁰, .. , value_def_n⁰ st`value

value_def1, ..

value_defn

value_def₁⁰ .. value_def_n⁰, {}

(4.8)

wherevalue_defi is an explicit value definition or an explicit function definition

c6=st

c`value_decl (4.9)

where value_decl is a value declaration

4.3.5.4 Transition system declarations

The following inference rule defines the translation operator for transition system declarations:

st`var_def1, .. , var_defnvar_def₁⁰, vs1, .. , var_def_n⁰, vsn

st`transition_system[s]

local var_def1, ..

var_defn

in

trans_rule1

[]

..

[]

trans_rule_n end

var_def₁⁰ .. var_def_n⁰, vs₁∪..∪vs_n

(4.10)

wherevar_def_i is a variable definition andtrans_rulei is a transition rule definition

iv`var_def1, .. , var_defnvar_def<sub>1</sub><sup>0</sup>, .. , var_def<sub>n</sub><sup>0</sup> iv`transition_system[s]

local var_def1, ..

var_def_n in

trans_rule₁ []

..

[]

trans_rulen

end

var_def₁⁰ .. var_def_n⁰

(4.11)

wherevar_defi is a variable definition andtrans_ruleiis a transition rule definition

tr, vs`trans_rule1, .. , trans_rulentrans_rule<sup>0</sup><sub>1</sub>, .. , trans_rule<sup>0</sup><sub>n</sub> tr, vs`transition_system[s]

local var_def1, ..

var_defn

in

trans_rule₁ []

..

[]

trans_rulen

end

trans_rule⁰₁||..||trans_rule⁰_n

(4.12)

where var_def is a variable definition andtrans_rule is a transition rule definition

c=ps

c`trans_sys_decl (4.13)

wheretrans_sys_decl is a type declaration

4.3.5.5 LTL assertion declarations

The following inference rules define the translation operatorfor LTL assertion declarations:

ps`ltl_def1, .. , ltl_defnltl_def<sub>1</sub><sup>0</sup>, .. , ltl_def<sub>n</sub><sup>0</sup> ps`ltl_assertion

ltl_def₁, ..

ltl_defn

ltl_def₁⁰ .. ltl_def_n⁰

(4.14)

whereltl_defi is a ltl assertion definition

c6=ps

c`ltl_decl (4.15)

whereltl_decl is a LTL assertion declaration declaration

4.3.5.6 Abbreviation type definitions

The following inference rule defines the translation operatorfor abbreviation type definitions:

type_exprtype_expr⁰

id=type_expr id==type_expr⁰ (4.16) wheretype_expr is a type name, type literal or a subtype expression

4.3.5.7 Variant type definitions

The following inference rule defines the translation operatorfor variant type definitions:

e1, .. , ene⁰₁, .. , e⁰_n

s==e₁|..|e_n s==e⁰₁|..|e⁰_n (4.17)

4.3.5.8 Explicit value definitions

The following inference rule defines the translation operatorfor explicit value definitions:

typetype⁰, ee⁰

s : type=e const type⁰ s==e⁰ (4.18)

4.3.5.9 Explicit function definitions

The following inference rule defines the translation operatorfor explicit func-tion definifunc-tions:

e₁, .. , e_ne⁰₁, .. , e⁰_n, type, .. , type_ntype⁰, .. , type⁰_n, veve⁰ id:type₁>< .. >< type_n→type

id(e1, .. , en)is ve

type⁰ id(type⁰₁e⁰₁, .. , type⁰_n e⁰_n){return ve⁰}

(4.19)

4.3.5.10 Variable definitions

The following inference rules define the translation operatorfor variable def-initions:

typetype⁰

st`s:type:=e s type⁰, {s} (4.20)

ee⁰

iv `s:type:=e s==e⁰ (4.21)

4.3.5.11 Transition rule definitions

The following inference rules define the translation operator for transition rule definitions:

Here all declared variables are updated in the transition rule vs\ {id1, .. , idn}=∅, bebe⁰, ve1, .. , venve⁰₁, .. , ve⁰_n

vs`be−→id⁰₁=ve1, .. , id⁰_n =ven

(be⁰&&id⁰₁==ve⁰₁&&..&&id⁰_n==ve⁰_n)

(4.22)

Here not all declared variables are updated in the transition rule vs\ {id1, .. , idn}={uc1, .. , ucm},

bebe⁰, ve₁, .. , ve_nve⁰₁, .. , ve⁰_n vs`be−→id⁰₁=ve₁, .. , id⁰_n =ve_n

(be⁰&&id⁰₁==ve⁰₁&&..&&id⁰_n==ve⁰_n

&&uc⁰₁==uc1&&..&&uc⁰_m==ucm)

(4.23)

4.3.5.12 LTL assertion definitions

The following inference rules define the translation operatorfor LTL assertion definitions:

bebe⁰

G(be) Globally[be⁰] (4.24)

bebe⁰

F(be) F inally[be⁰] (4.25)

bebe⁰

X(be) N ext[be⁰] (4.26)

be₁be⁰₁, be₂be⁰₂

U(be1, be2) [be⁰₁]U ntil[be⁰₂] (4.27)

4.3.5.13 Identifiers

The following inference rule defines the translation operatorfor identifiers:

e e (4.28)

wheree is an identifier

4.3.5.14 Operators

The following inference rules define the translation operator for operators.

Note that the operator used in the intermediate language is different in some cases, such as ∧ becoming &&. This is such that the intermediate language matches the existingtoString methods and parsers used in RT-Tester.

=== (4.29)

++ (4.30)

−− (4.31)

∗∗ (4.32)

// (4.33)

<< (4.34)

>> (4.35)

≤≤ (4.36)

≥≥ (4.37)

∨|| (4.38)

∧&& (4.39)

∼! (4.40)

4.3.5.15 Type names

The following inference rule defines the translation operatorfor type names:

typetype (4.41)

4.3.5.16 Type literals

The following inference rules define the translation operatorfor type literals:

Int int (4.42)

Real real (4.43)

Bool bool (4.44)

4.3.5.17 Subtype expressions

The following inference rule defines the translation operatorfor subtype ex-pressions:

typetype⁰, veve⁰

s1={|s2 : type:−ve|} s1==type⁰s2where ve⁰ (4.45)

4.3.5.18 Variable names

The following inference rule defines the translation operator for variable names:

idid (4.46)

4.3.5.19 Value names

The following inference rule defines the translation operatorfor value names:

idid (4.47)

4.3.5.20 Value literals

The following inference rule defines the translation operatorfor value literals:

e e (4.48)

wheree is a value literal

4.3.5.21 Function application expressions

The following inference rule defines the translation operatorfor function ap-plication expressions:

ve1, .. , venve⁰₁, .. , ve⁰_n

id(ve1, .. , ven)id(ve⁰₁, .. , ve⁰_n) (4.49)

4.3.5.22 Value infix expressions

The following inference rules define the translation operator for value infix expressions:

ve₁ve⁰₁, ve₂ve⁰₂, opop⁰

ve1op ve2 ve⁰₁op⁰ve⁰₂ (4.50) where ve₁ andve₂ are in normal form

ve1≡rw_ve1, ve2≡rw_ve2, rw_ve₁op rw_ve₂≡rw_inf ix, rw_inf ixrw_inf ix⁰

ve₁op ve₂ rw_inf ix⁰ (4.51)

4.3.5.23 Value prefix expressions

The following inference rules define the translation operatorfor value prefix expressions:

veve⁰

∼ve!ve⁰ (4.52)

whereve is in normal form

ve≡rw_ve,∼rw_ve≡rw_pref ix, rw_pref ixrw_pref ix⁰

∼ve rw_pref ix⁰ (4.53)

4.3.5.24 If expressions

The following inference rules define the translation operatorfor if expressions:

If expression with elsif-branches

ifbethenve1elsif_branchelseve2end≡rw_if_expr, rw_if_exprif_expr⁰

ifbethenve1elsif_branchelseve2endif_expr⁰ (4.54) whereelsif_branch is an elsif branch and

whereve1 andve2 are boolean expressions If expression without elsif-branches

bebe⁰, ve1ve⁰₁, ve2ve⁰₂ if bethenve1elseve2end

((be⁰ &&ve⁰₁)||(!(be⁰) &&ve⁰₂))

(4.55)

whereve1 andve2 are boolean expressions and wherebe,ve1 andve2 are in normal form

be≡rw_be, ve1≡rw_ve1, ve2≡rw_ve2,

if rw_bethenrw_ve₁elserw_ve₂rw_if_expr⁰ end

if bethenve1elseve2endrw_if_expr⁰ (4.56) whereve₁ andve₂ are boolean expressions

4.3.5.25 Case expressions

Note that case expressions are not translated directly, but rather rewritten into an equivalent if expression and then translated.

The following inference rule defines the translation operatorfor case expres-sions:

case_expr≡if_expr, if_exprif_expr⁰

case_exprif_expr⁰ (4.57)

wherecase_expr is a case expression

4.3.5.26 Rewriting value expressions

The following inference rules define the rewriting operator ≡for value expres-sions.

The inference rules below should be applied in the order they are presented, such that the first rule has the highest priority. An example showing the use of these rules can be found in AppendixA.2.

Rewrite case expression into equivalent if expression

ve1, .. , ven+1≡rw_ve1, .. , rw_ven+1

caseeof e1→ve1

e2→ve2

..

e_n→ve_n _→ven+1

≡

if e=e1thenrw_ve1else ife=e2thenrw_ve2else

..

if e=enthenrw_venelserw_ven+1end ..

end end

(4.58)

Rewrite if expression containing else if branches

ve≡rw_ve, ve1, .. , ven≡rw_ve1, .. , rw_ven, be₁, .. , be_n≡rw_be₁, .. , rw_be_n

if be₁thenve₁ elsif be2thenve2

..

elsif benthenven

elseveend

≡

if rw_be1thenrw_ve1else if rw_be₂thenrw_ve₂else

..

if rw_be_nthenrw_ve_nelserw_ve ..

end end

(4.59)

Rewrite two if expressions used in the same value expression

ve₁≡rw_ve₁, ve⁰₁≡rw_ve⁰₁, ve₂≡rw_ve₂, ve⁰₂≡rw_ve⁰₂, be1≡rw_be1, be2≡rw_be2

rw_ve₁op rw_ve₂≡rw_inf ix₁, rw_ve₁op rw_ve⁰₂≡rw_inf ix₂, rw_ve⁰₁op rw_ve2≡rw_inf ix3, rw_ve⁰₁op rw_ve⁰₂≡rw_inf ix4

if be1thenve1elseve⁰₁end op

if be2thenve2elseve⁰₂end

≡

if rw_be1∧rw_be2thenrw_inf ix1else if rw_be1∧ ∼rw_be2thenrw_inf ix2else

if ∼rw_be₁∧rw_be₂thenrw_inf ix₃elserw_inf ix₄ end

end end

(4.60)

Rewrite if expression used in infix value expression (right)

be≡rw_be, ve1≡rw_ve1, ve2≡rw_ve2

e op rw_ve1≡rw_inf ix1, e op rw_ve2≡rw_inf ix2

e opif bethenve1elseve2end

≡

if rw_bethenrw_inf ix1elserw_inf ix2end

(4.61)

Rewrite if expression used in infix value expression (left)

be≡rw_be, ve1≡rw_ve1, ve2≡rw_ve2

rw_ve1op e≡rw_inf ix1, rw_ve2op e≡rw_inf ix2

if bethenve1elseve2endop e

≡

if rw_bethenrw_inf ix₁elserw_inf ix₂end

(4.62)

Rewrite if expression used in prefix value expression be≡rw_be, ve1≡rw_ve1, ve2≡rw_ve2

∼(if bethenve1elseve2end)

≡

ifrw_bethen ∼(rw_ve₁)else ∼(rw_ve₂)end

(4.63)

No if expressions to rewrite

ve≡ve (4.64)

whereve is in normal form

ve1≡rw_ve1, ve2≡rw_ve2, rw_ve1op rw_ve2≡rw_inf ix

ve1op ve2≡rw_inf ix (4.65)

In document Bounded Model Checking for RSL using RT-Tester (Sider 54-72)