K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

Dear all, 
I'm Daniele, first year PhD student at Imperial College London.
I came across K a couple of weeks ago and I'm not familiar with rewriting 
logic (I'm more used to think in terms of big-step operational semantics), so 
I hope my questions will not be too boring.

I'm trying to write a rule for reference assignment as found in PHP: 

> x = 5;
> y = &x; // <---

Basically I want to assign to variable $y the address of variable $x. 
However, this "references" are not pointers as in C, but they just provide 
variable aliasing. It is wrong to do something like 'y = &x + 1' and so on. 
Moreover, '&x' itself its not an expression in the language (I saw that 
something like this is done in CHALLENGE, in the paper 'An Overview of the K 
Semantics Framework, but my case looks different).

What i need to do is: when a statement 'X:Id := & Y:Id' is found:
  - look in the environment (mapping var. names to addresses). If Y is mapped 
to address N, then update the environment by mapping also X to N. 

I've been trying to write some rules, but none of them works. I suspect that 
the operation cannot be expressed 'atomically' in K. My first trial was 
something like:

> rule [ass_ref_1]:
>     <k> X := & Y:Id => . ... </k>
>     <env> ... Y |-> N => X |-> N  ... </env>


but of course it is wrong because it 'destroys' the mapping of Y into address 
N.
I tried several variations on this but with no luck. I think that the problem 
lies in the fact that I have to 'rewrite' in some way what I match (the 
mapping Y |-> N in this case). But I don't want to rewrite, I want to add 
another mapping, X |-> N. Maybe I have to split this operation into two or 
more simpler ones?

I was also thinking about using 'when':

> rule [ass_ref_1]:
>     <k> X := & Y:Id => . ... </k>
>     <env> Rho:Map => Rho[N\X]  </env>
> when <condition on Rho saying that Y |-> N> 


The problem here is that I can't find the appropriate condition. I didn't 
found any documentation, and on the tutorials there is just the 'in Keys Rho' 
condition. 

Any advice? Thanks a lot!

Kind Regards, 
Daniele Filaretti