K-user mailing list

[Radu Mereuta <headness13 AT gmail.com>]

Hi Samira,

Did you put strict(2) as an attribute to the assignment syntax declaration?

Something else that I've noticed is the task rule. Variable I should be of type Int. That way the rule will apply only after the _expression_ on the right hand side of assignment will be evaluated.

Radu

K-developer

On Wed, Jul 3, 2013 at 1:46 PM, samira kherfellah <samira.kherfellah AT gmail.com> wrote:

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.

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user