K-user mailing list

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

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