K-user mailing list

[Dorel Lucanu <dlucanu AT info.uaic.ro>]

Dear Charles,

Thanks for your message.
The configuration abstraction mechanism is a bit more complex than that used for list.
The main idea is that the context transformation algorithm (which reconstruct the subconfiguration from the abstract one) maps the cells  from rules  to configuration such that the implied configuration is minimal;  this is called "locality principle" in An Overview of the K Semantic Framework by Grigore Rosu and Traian Florin Serbanuta (see the publication list).
So, the context transformation algorithm produces exact the configuration written at the end of your message.

Bests,
Dorel

On 08.06.2013 4:19, Charles Jacobsen wrote:

Greetings ---

Are the semantics of built-in lists, sets, and bags available? For example, I found the following simple rule natural, but wanted to see why it works (looking at the relevant rule):

<some-list-cell> ... (.List => ListItem(15)) ... </some-list-cell>

This means we can insert anywhere in a list.

This next rule is a bit perplexing, due to the configuration abstraction (found in the imp++ tutorial):

rule <k> spawn S => T ...</k> <env> Rho </env>
       (. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)

It seems like the implied configuration, wrapping this, is:

rule <thread>
        <k> spawn S => T ...</k> <env> Rho </env>
        (. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
     </thread>

as only <k> and <env> cells appear in <thread> cells; but I think that is not correct. I think the implied configuration is:

rule <threads>
        ...       
        <thread>
           ...
           <k> spawn S => T ...</k>
           <env> Rho </env>
           ...
        </thread>

        (. => <thread>... <k> S </k> <env> Rho </env> <id> T </id> ...</thread>)
        ...
     </threads>

Is that correct? I am not sure.

Charlie (undergrad)

_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user

-- 
======================================
Dorel Lucanu, Ph.D.
Department of Computer Science, director
Faculty of Computer Science
Alexandru Ioan Cuza University
Berthelot 16, 700483 Iasi, Romania
URL: www.infoiasi.ro/~dlucanu
Tel.: +40 232 201551
Fax.: +40 232 201490
======================================