K-user mailing list

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

Hi All,

I have a question about declaring variables in K. 

Here is an example of using variables in my language

var i integer ;

...

task i := i+1; 

...

The variables must be initialized to 0, the rules are defined as follows:

rule <k> var X:Id TV:Type ;  => . ...</k> 

      <tenv>... . => X |-> TV ...</tenv> 

      <store>... . => X |-> 0 ...</store> 

// lookup

rule <k> X:Id => V ...</k>

<store>... X |-> V ...</store> 

rule <k>  task X:Id := I:Int ; => . ...</k> 

<store>... X |-> (_=> I) ...</store> 

<tenv>... X |-> integer ...</tenv>

this way is it correct or there is something else to add? how to initialize variables to 0?

Thanks.

Samira.