K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

Thank you both, I'm going to check it.

Cheers, 

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