K-user mailing list

[samira kherfellah <samira.kherfellah AT gmail.com>]

Hi All,

in my program, we can use variables like this:

var x integer ;
.
.
.

task x := x + 1 ;

Variables are initialized to 0.

To do this in k, I add the rules:

rule <k> var X:Id TV:TypeVar ;  => . ...</k>
      <tenv>... . => X |-> TV ...</tenv>
      <store>... . => X |-> 0 ...</store>


//task
rule <k>  task X:Id := I:Exp ; => . ...</k>
<store>... X |-> (_=> I) ...</store>
<tenv>... X |-> integer ...</tenv>

//_expression_
rule I1:Int + I2:Int => I1 +Int I2

But at execution, I have the result:

<tenv> x |-> integer </tenv>

<store> x |-> x + 1 </store>

and not

<tenv> x |-> integer </tenv>
<store> x |-> 1 </store>

I want to display the result of the _expression_ "x + 1" and not the _expression_ "x + 1"

Samira.