K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

On 23 Jul 2012, at 14:45, Rosu, Grigore wrote:

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).

Well, probably there's still something missing (it is still a work in progress), but all the relevant features are already there (including scopes, prototype chains, functions, assignment, this construct, with construct, new, delete, sequence, conditional, while loops, basic unary and binary operators, and typeof...). 

In fact one of the goals was to have a comprehensive definition, without dropping too many inconvenient features.

 

The semantics is executable in the sense that we have developed an interpreter and proved it correct w.r.t. the semantics (everything done in Coq, the interpreter can then be extracted to OCaml or Haskell).  

I cc my supervisor Sergio Maffeis, as he may be interested.

Kind regards, 

Daniele

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