k-user AT lists.cs.illinois.edu
Subject: K-user mailing list
List archive
- From: Traian Florin Şerbănuţă <traian.serbanuta AT fmi.unibuc.ro>
- To: imran.pcs16 AT iitp.ac.in, k-user AT lists.cs.illinois.edu
- Subject: Re: [[K-user] ] K rule for if-else statement regarding
- Date: Thu, 23 Jun 2016 13:18:19 +0000
Hi Imran,
Since it seems you want to execute both branches and to "join" their results, one suggestion would be two use a "stack" of memory frames, one for each nested conditional, where writes would only be done at the top level, while lookups would be done in the most recent frame containing the location being looked up.
On Thu, Jun 23, 2016 at 3:33 PM <imran.pcs16 AT iitp.ac.in> wrote:
Hi, This is Imran from India. I am using K Framework for static
flow-sensitivity in Imperative language. Here every program variable and
constant initialized with 'low' and if a variable assigned with user input
then we mapped it to 'high' and if this variable used in any computation
with some other variable then other variable will be mapped to 'high'. For
example, Consider the following code:
int x,y; // x,y initially mapped with 'low'
x= input(user); // x mapped to high due to input from user
y=x; // As x is mapped to high, y will be mapped to high.
I am unable to to write rule for conditional statements like if-else.
Suppose a variable 'X' mapped to 'high' in if-part and 'low' to else-part.
After the execution of if-else statement ,variable should map to 'high' as
well as 'low'. If any further assignment of 'X' comes after if-else
statement, then 'X' mapping would remain same(i.e, X |-> (high,low) ). For
example, Consider the following code:
int x,y;
x = input(..);
if(...){
y = x; // 'y' mapped to 'high' as 'x' is 'high'
}
else{
y = 10; // y mapped to 'low'
}
-----
-----
Kindly suggest some rule to do the above task.
With Regards
Imran
- [[K-user] ] K rule for if-else statement regarding, imran . pcs16, 06/23/2016
- Re: [[K-user] ] K rule for if-else statement regarding, Traian Florin Şerbănuţă, 06/23/2016
Archive powered by MHonArc 2.6.16.