We present here how to define the semantics of a simple programming language
with skip, assignment, If statement, While
loop, and composition of instructions in the line of WhileL. We assume some knowledge
of the theoretical transformations performed by the tool.
First, we define the syntax of the programming language in the WHILE-SYNTAX-EVAL,
which includes the QID module to define variables.
(fmod WHILE-SYNTAX-EVAL is protecting QID .
We declare the sorts Var for the numerical variables, Num for numbers,
Op for binary numerical operators, Exp for numerical expressions, BVar
for boolean variables, Boolean for Boolean values, BOp for binary Boolean operators,
BExp for Boolean expressions, Com for commands, and Prog for
programs. A Qid can be used as a variable, which can be used as an expression, while a
natural number can be used as a value of sort Num, which is also an expression; an analogous
subsort declaration is used for boolean values. Finally, a program is just a supersort of a command, possibly
built by using composition.
sorts Var Num Op Exp BVar Boolean BOp BExp Com Prog . subsorts Qid < Var < Exp . subsort Nat < Num < Exp . subsorts Qid < BVar < BExp . subsort Boolean < BExp . subsort Com < Prog .
We define the constants w, x, y, and z
for variables and +., -., and *. as operators (where the dot is used
to distinguish these operators from the predefined ones). Similarly, T and F are
declared for true and false, respectively, while And and Or
are Boolean operators:
ops w x y z : -> Var . ops +. -. *. : -> Op . ops T F : -> Boolean . ops And Or : -> BOp [format(! o)] .
Expressions are built by using two expressions of the appropriate type and a binary operator or by using the
special operators Not, which is unary, and Equal, which takes two numerical expressions
and returns a Boolean expression:
op ___ : Exp Op Exp -> Exp [prec 20] . op ___ : BExp BOp BExp -> BExp [prec 20] . op Not_ : BExp -> BExp [prec 15 format(! o o)] . op Equal : Exp Exp -> BExp [format(! o)] .
Finally, we define the possible commands in the usual way:
op skip : -> Com [format(!r o)] . op _:=_ : Var Exp -> Com [prec 30 format(i d d d)] . op _;_ : Com Com -> Com [prec 40 gather(e E) format(i d ni d)] . op If_Then_Else_ : BExp Com Com -> Com [prec 50 format(i! o ! on++ --!n on++ --o)] . op While_Do_ : BExp Com -> Com [prec 60 format(i! o ! on++ --no)] . endfm)
The AP-EVAL module imports the one above and is in charge of defining the semantics of the application
of the binary operators:
(fmod AP-EVAL is pr WHILE-SYNTAX-EVAL . op Ap : Op Num Num -> Num . vars n n' : Num . eq Ap(+., n, n') = n + n' . eq Ap(*., n, n') = n * n' . eq Ap(-., n, n') = if n < n' then 0 else sd(n, n') fi . op Ap : BOp Boolean Boolean -> Boolean . var bv bv' : Boolean . eq Ap(And, T, bv) = bv . eq Ap(And, F, bv) = F . eq Ap(Or, T, bv) = T . eq Ap(Or, F, bv) = bv . endfm)
The module ENV-EVAL defines the current state of the variables. To do so, it first specifies
the sorts Value and Variable for values and variables, respectively:
(fmod ENV-EVAL is pr WHILE-SYNTAX-EVAL . sorts Value Variable . subsorts Num Boolean < Value . subsorts Var BVar < Variable .
Then, the sort ENV is used to define this state. The constant mt stands for the
empty state, while the operator _=_ is used to bound a value to a variable. Bigger states are built
with the juxtaposition operator:
sort ENV . op mt : -> ENV . op _=_ : Variable Value -> ENV [prec 20] . op __ : ENV ENV -> ENV [assoc id: mt prec 30] .
We also define some functions for looking for values into the state and update it:
op _`[_/_`] : ENV Value Variable -> ENV [prec 35] . op remove : ENV Variable -> ENV . op _`(_`) : ENV Var -> Num .
These functions are implemented in the usual way:
vars X X' : Variable . var V : Value . var ro : ENV . eq remove(mt, X) = mt . eq remove(X = V ro, X') = if X == X' then ro else X = V remove(ro,X') fi . eq ro [V / X] = remove(ro,X) X = V . eq (X = V ro)(X') = if X == X' then V else ro(X') fi . endfm)
The module EVALUATION-EXP-EVAL defines by means of rules how the expressions
are evaluated. It defines a new sort Statement that stands for pairs of expressions
and states, indicating that the expression is evaluated in the given state:
(mod EVALUATION-EXP-EVAL is protecting ENV-EVAL . protecting AP-EVAL . sort Statement . subsorts Value < Statement . op <_`,_> : Exp ENV -> Statement . op <_`,_> : BExp ENV -> Statement .
The first rule, CR, indicates that a number is evaluated to itself:
var n : Num . var X : Var . var st : ENV . vars e e' : Exp . var op : Op . vars v v' : Num . var bx : BVar . vars bv bv' : Boolean . var bop : BOp . vars be be' : BExp . rl [CR] : < n, st > => n .
The rule VarR rewrites a variable to its value in the state:
rl [VarR] : < X, st > => st(X) .
The rule OpR is in charge of evaluating expressions using binary operators. It first
evaluates the sub-expressions in the conditions and then uses the function Ap shown above
to compute the final result:
crl [OpR] : < e op e', st > => Ap(op,v,v')
if < e, st > => v /\
< e', st > => v' .
The rules BCR1 and BCR2 indicate that T and F
are evaluated to themselves:
rl [BCR1] : < T, st > => T . rl [BCR2] : < F, st > => F .
Similarly to the rule VarR above, BVarR evaluates a Boolean variable by
checking the current state:
rl [BVarR] : < bx, st > => st(bx) .
The rule BOpR evaluates a Boolean expression by first evaluation the sub-expressions
in the conditions:
crl [BOpR] : < be bop be', st > => Ap(bop,bv,bv')
if < be, st > => bv /\
< be', st > => bv' .
The rules EqR1 and EqR2 are in charge of evaluating the Equal
operator. If the two sub-expressions are evaluated to the same value the whole expression is evaluated
to T, and it is evaluated to F otherwise:
crl [EqR1] : < Equal(e,e'), st > => T
if < e, st > => v /\
< e', st > => v .
crl [EqR2] : < Equal(e,e'), st > => F
if < e, st > => v /\
< e', st > => v' /\ v =/= v' .
Finally, the rules Not1 and Not2 evaluate the Not operator as
usual:
crl [Not1] : < Not be, st > => F
if < be, st > => T .
crl [Not2] : < Not be, st > => T
if < be, st > => F .
endm)
The module EVALUATION-WHILE specifies the evaluation semantics of the whole language. It
extends the sort Statement with a new operator that puts together commands and states:
(mod EVALUATION-WHILE is pr EVALUATION-EXP-EVAL . op <_`,_> : Com ENV -> Statement .
The rule AsR defines the semantics of the assignment. It first evaluates the expression
that is going to be assigned and then updates the current state:
var X : Var .
vars st st' st'' : ENV .
var e : Exp .
var v : Num .
var be : BExp .
vars C C' C'' : Com .
crl [AsR] : < X := e, st > => < skip, st[v / X] >
if < e, st > => v .
The rules IfR1 and IfR2 are in charge of the semantics of the If
statement. They first evaluate the condition and then distinguish whether its value is T or
F. If the former happens then the command in the Then branch is executed in the
conditions and its value returned in the obtained state; otherwise, the Else branch is used:
crl [IfR1] : < If be Then C Else C', st > => < skip, st' >
if < be, st > => T /\
< C, st > => < skip, st' > .
crl [IfR2] : < If be Then C Else C', st > => < skip, st' >
if < be, st > => F /\
< C', st > => < skip, st' > .
The rule ComR describes the composition of commands. It uses the conditions to execute the
first one and then execute the rest of them in the new state:
crl [ComR] : < C ; C', st > => < skip, st'' >
if < C, st > => < skip, st' > /\
< C', st' > => < skip, st'' > .
Finally, the rules WhileR1 and WhileR2 deal with the While loop.
They distinguish whether the condition is evaluated to T or F to evaluate the body
of the instruction or finish the execution:
crl [WhileR1] : < While be Do C, st > => < skip, st >
if < be, st > => F .
crl [WhileR2] : < While be Do C, st > => < skip, st' >
if < be, st > => T /\
< C ; (While be Do C), st > => < skip, st' > .
endm)
Now we can write and evaluate programs in this language. For example, we can define the program ex
in the module TESTING:
(mod TESTING is
pr EVALUATION-WHILE .
op init : -> Statement .
eq init = < (If Equal(x, 0) Then y := 0
Else y := 1) ;
(If Equal(w, 0) Then z := 0
Else z := 1), st:ENV > [nonexec] .
op ex : -> Statement .
eq ex = < (If Equal(x, 0) Then y := 0
Else y := 1) ;
(If Equal(w, 0) Then z := 0
Else z := 1), x = 0 w = 0 > .
endm)
Note that we also define a term init that will be used later. We can compute the result for
ex with:
Maude> (rew ex .) rewrite in EVALUATION-WHILE : ex result Statement : < skip, x = 0 w = 0 y = 0 z = 0 >
However, we may be interested on testing this program for all the possible initial states (or at least for all the significant initial states). We can use our tool for this purpose: Once all the modules have been introduced in Full Maude and the tool has been started, we can indicate the module where testing must take place and the sort of the statements that we want to cover with the following commands:
Maude> (semantics module TESTING .) Module TESTING selected for semantics testing. Maude> (set sort statements Com .) Sort Com selected as sort of statements.
Once these commands are introduced the tool manipulates the rules in the (flattened)
TESTING module as described in the previous section. We can display
these modified rules with:
Maude> (show semantics rules .)
Rule extraInfo-IfR1 :
crl < stmntIndx(If be:BExp Then stmntIndx(C:Com,V$#0:Nat)
Else stmntIndx(C':Com,V$#1:Nat),V$#2:Nat),st:ENV >
=> < skip,st':ENV >
if < be:BExp,st:ENV > => T /\
< stmntIndx(C:Com,V$#0:Nat),st:ENV > => < skip,st':ENV > .
Rule extraInfo-AsR :
crl < stmntIndx(X:Var := e:Exp,V$#0:Nat),st:ENV >
=> < skip,st:ENV[v:Num / X:Var]>
if < e:Exp,st:ENV > => v:Num .
...
where we see that each possible term of sort Com, which is the sort we want to cover, has been paired
with a fresh variable of the form V$# by means of the constructor stmntIndx.
Now it is worth seeing the
map between the rules and the executed statements. The tool follows a simple strategy to generate
this map that consists of selecting as executed statement the first term of the given sort found (i)
in the lefthand side of the rule, traversed following a width-first search in the tree representing
the term; or (ii) in the conditions if the lefthand side does not contain a term of this sort.
Note that, although this strategy is quite simple, it works very well in practice because, when several
statements appear in a term, the outermost is the one usually applied (e.g. to direct the execution of
the inner ones). The command in charge of showing this information is:
Maude> (show applied statements .) The rule extraInfo-AsR : crl < stmntIndx(X:Var := e:Exp,V$#0:Nat),st:ST > => < skip,st:ST[v:Num / X:Var]> if < e:Exp,st:ST > => v:Num . applies the statement X:Var := e:Exp identified by the variable V$#0 ...
If the tool fails to associate the appropriate information to a rule, the following commands can be used:
Maude> (rule Q is not associated to any statement .) The mapping for rule Q has been updated. Maude> (rule Q is associated to VL .) The mapping for rule Q has been updated.
where Q is a rule label and VL is the list of variables
identifying the applied statements.
We can now introduce the program we want to test with the following command:
Maude> (object program init .) Object program introduced.
Since we may be interested in only covering some of the statements of the initial coverage (e.g., because we want to know whether a specific one, such as an exception, is reached). The user can modify the statements in the coverage with:
Maude> (statements in coverage NL .) The required coverage has been updated.
where NL is a list of natural numbers indicating the statements to be covered.
When all the options have been set, we can start the testing process. The current
version of the tool only supports, as explained in the previous section, the global branch
coverage strategy, and thus the following result is obtained:
Maude> (start semantics testing .) 2 test cases must be checked by the user: The program reaches the state < skip, x = 0 y = 0 w = 0 z = 0 > starting with the substitution st:ST |-> x = 0 y = 0 w = 0 z = 0 and covers the statements 1, 2, 4, 5 The program reaches the state < skip, x = 1 y = 1 w = 1 z = 1 > starting with the substitution st:ST |-> x = 1 y = 0 w = 1 z = 0 and covers the statements 1, 3, 4, 6 All the statements were covered