K-user mailing list

["Rosu, Grigore" <grosu AT illinois.edu>]

Almost right.  It may actually work right, but it is semantically incorrect.  Remove the "..."s from the env cell in the second rule, because you want to make sure that Rho matches the entire cell contents except for the binding of Y.

Also, you need another rule for when X and Y are equal.  Alternatively, you can do everything with one rule of the form

rule

  <k> X := &Y => . </k>

  <env> Rho => Rho[X <- Rho[Y]] </env>

(check the precise syntax of map updates, as I do not remember it precisely now).

However, although more compact, if you are a K puritan then you may not like this semantics because it seriously inhibits the true concurrency of your definition: this rule grabs and writes the entire environment, so no other rule can concurrently touch the environment (think of K rules as transactions). If you are OK with an interleaving semantics, then the one-rule semantics above, or something similar, may be your best choice here.

Cheers,

Grigore

 

 

---

From: Daniele Filaretti [dfilaretti AT gmail.com]
Sent: Monday, July 23, 2012 10:36 AM
To: Rosu, Grigore
Cc: Mark Hills; k-user AT cs.uiuc.edu
Subject: Re: [K-user] new user: assignment by reference (as in PHP) and available operations on "Maps"

Yes, you were right. Ok, so I splitted the rule into two, one for the case when X is new and one for the case when it is already bound:

rule [ass_ref_old]:         // X already bound in environment

    <k> X := & Y:Id => . ... </k>

    <env> ... Y |-> N ... (X |-> (_ => N)) ... </env>

    

rule [ass_ref_new]:         // X fresh in the environment

    <k> X := & Y:Id => . ... </k>

    <env> ... Rho:Map( Y |-> N ) ... (. => Rho[X |-> N])...  </env>

        when notBool(X in keys(Rho))

Is it what you meant?

It seems to work fine now. 

Many thanks! 

Daniele

On 23 Jul 2012, at 15:16, Rosu, Grigore wrote:

That is correct, thanks Mark.  Daniele, you can take a look at our IMP language, to see how to check whether an environment already contains a binding or not.

Grigore

 

 

---

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Mark Hills [Mark.Hills AT cwi.nl]
Sent: Monday, July 23, 2012 9:13 AM
To: Daniele Filaretti; k-user AT cs.uiuc.edu
Subject: Re: [K-user] new user: assignment by reference (as in PHP) and available operations on "Maps"

Just a quick comment: the rules given below seem to assume that X is not yet bound, i.e., not yet in the environment. It would be good to check this first, since I'm assuming that adding new mappings into the environment in the way being done below won't remove any existing mappings (if this isn't true, please feel free to correct me).

Cheers,

Mark

On Monday, July 23, 2012 at 3:45 PM, Rosu, Grigore wrote:

Maurice Rabb is our student who is defining _javascript_, so I hope he can tell you more about it. I have never compiled or run the _javascript_ semantics yet.

Just curious: have you defined the ENTIRE _javascript_? When we defined C and looked into the existing C definitions, we found that all previous semantics were quite partial, dropping "inconvenient" features (e.g., longjumps, goto, etc.). Also, is your _javascript_ semantics executable? We are also very interested in defining an executable semantics of _javascript_ in K, and then to use it to verify programs (using the methodology in our OOPSLA'12 paper).

Regarding our K2Coq translator, we only have plans so far and concrete ideas, maybe even a rough prototype, but we are not there yet. We'd like to do several backends at the same time: Coq, PVS, ACL2. All these need almost the same transformations on the K definitions, except for a last step which turns things into the target language.

Cheers,

Grigore

p.s. I CCed the k-user list.

________________________________________

From: Daniele Filaretti [dfilaretti AT gmail.com]

Sent: Monday, July 23, 2012 8:26 AM

To: Rosu, Grigore

Subject: Re: [K-user] new user: assignment by reference (as in PHP) and available operations on "Maps"

It works! Thank you Stefan and Grigore!

...I have a couple of other (non technical) questions: I read somewhere that there is a future plan for implementing Coq output from K. Is there any updated information available? That would be very interesting (by the way: we've formalised _javascript_ in Coq, this is the website if someone is interested: http://jscert.org/)

Last one: in the example folder of K there is a _javascript_ project; I've been trying to compile the pdf but it didn't work (after one day it was still running:). Does anybody have that pdf? I would be happy to have a look at it.

Many thanks again,

Daniele

On 23 Jul 2012, at 13:58, Rosu, Grigore wrote:

Or even nicer (in the K sense):

rule [ass_ref_1]:

<k> X := & Y:Id => . ...</k>

<env>... Y |-> N (. => X |-> N) ...</env>

If the current K parser gives you headaches, you may try to write .Map instead of .

Welcome to K, Daniele,

Grigore

________________________________________

From: k-user-bounces AT cs.uiuc.edu [k-user-bounces AT cs.uiuc.edu] on behalf of Stefan Ciobaca [stefan.ciobaca AT gmail.com]

Sent: Monday, July 23, 2012 7:54 AM

To: Daniele Filaretti

Cc: k-user AT cs.uiuc.edu

Subject: Re: [K-user] new user: assignment by reference (as in PHP) and available operations on "Maps"

Hello Daniele,

Welcome to K. I'll try to answer your question directly:

rule [ass_ref_1]:

<k> X := & Y:Id => . ... </k>

<env> ... Y |-> N => X |-> N ... </env>

Did you try to do the following?

rule [ass_ref_1]:

<k> X := & Y:Id => . ... </k>

<env> ... Y |-> N => (Y |-> N X |-> N) ... </env>

This replaces Y |- N by both X |- N and Y |- N, so it keeps Y bound. I

hope it solves your problem. Let us know if it works for you.

Cheers,

Stefan

_______________________________________________

k-user mailing list

k-user AT cs.uiuc.edu

http://lists.cs.uiuc.edu/mailman/listinfo/k-user

_______________________________________________

k-user mailing list

k-user AT cs.uiuc.edu

http://lists.cs.uiuc.edu/mailman/listinfo/k-user