K-user mailing list

["Moore, Brandon Michael" <bmmoore AT illinois.edu>]

Hi Samira.

I haven't tested it, but that looks reasonable. Are you having any problems with it?

Brandon

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of samira kherfellah [samira.kherfellah AT gmail.com]
Sent: Friday, August 30, 2013 10:58 AM
To: k-user AT cs.uiuc.edu
Subject: [K-user] Variable declaration

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.