K-user mailing list

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

Sorry, I said that your rule would be

  rule [assign-create]:
             <k> X = I:Int; => . ... </k>
             <env> M:Map => M[?L/X] </env>
             <store> ... . => ?L |-> I ... </store>
             <nextAddr> I:Int => I +Int 1 </nextAddr>)
    requires notBool (X in keys(M)) andBool ?L = alloc()

which is incorrect.  It would be

  rule [assign-create]:
             <k> X = I:Int; => . ... </k>
             <env> M:Map => M[?L/X] </env>
             <store> ... . => ?L |-> I ... </store>
             <nextAddr> I:Int => I +Int 1 </nextAddr>)
    requires notBool (X in keys(M))
    ensures ?L = alloc()

Grigore



________________________________________
From: 
k-list-bounces AT cs.uiuc.edu
 
[k-list-bounces AT cs.uiuc.edu]
 on behalf of Rosu, Grigore 
[grosu AT illinois.edu]
Sent: Wednesday, July 09, 2014 7:33 AM
To: Moore, Brandon Michael; Daniele Filaretti; 
k-user AT cs.uiuc.edu
Cc: 
k-list AT cs.illinois.edu
Subject: Re: [k-list] [K-user] matching entire configuration while also 
matching        its     components

Brandon is right, that is an acceptable solution for now.

However, we, the K developers, should do what we discussed for a long time to 
do, namely to allow functions to have access to the entire state.  We will 
take this task seriously over the next few weeks, and hopefully the next 
release of K will include it.  Here is how your example rule will look like 
then:

  rule [assign-create]:
             <k> X = I:Int; => . ... </k>
             <env> M:Map => M[?L/X] </env>
             <store> ... . => ?L |-> I ... </store>
             <nextAddr> I:Int => I +Int 1 </nextAddr>)
    requires notBool (X in keys(M)) andBool ?L = alloc()

?L means that it is an existentially quantified "fresh" variable in the RHS 
of the rule, which is further constrained by the equality ?L = alloc().  You 
do not want to write alloc() twice in the RHS, because you may not want to 
propagate the side-effects of the function alloc() on the state twice.  For 
example, alloc() can be defined something like this:

  rule alloc() => "L" +String int2string(N)
       <nextLoc> N => N +Int 1 </nextLoc>

Would this be acceptable?

Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Moore, Brandon Michael 
[bmmoore AT illinois.edu]
Sent: Tuesday, July 08, 2014 11:15 AM
To: Daniele Filaretti; 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] matching entire configuration while also matching its   
  components

I don't know of any easy way to grab everything like that. I think you just 
have to explicitly name the "rest" of every cell, and put it together 
yourself.

Cutting down to one call to alloc would help, if you need to explicitly 
assemble the state yourself.
You can define a new kind of item to put in the K cell to hold and use the 
result, like this:

  rule [assign-create]:
             <k> X = V:Int; => do_alloc(X
            
alloc(Bag(<k>KRest</k><env>M</env><store>S</store><nextAttr>I</nextAddr>),V) 
KRest </k>
             <env>M</env>
             <store>S</store>
             <nextAddr>I</nextAddr>
         when notBool (X in keys(M))

(I changed "I" to "V" in the assignment, assuming you didn't mean the rule to 
apply only when you were asigning a value that happened to match nextAddr).

then you give do_alloc semantics with a rule like
  rule [do-alloc]:
             <k> do_alloc(X,Loc,V) => . ...</k>
             <env>M => M[Loc/X]</env>
             <store>... . => Loc |-> V ...</store>
             <nextAddr> I => I+Int 1 </nextAddr>

We've thought a little bit about whether there is some way to give rules 
read-only access to the whole configuration (or maybe cell completion style 
access to cells near the call?), but don't have any concrete design or plans 
for it.
Maybe you could say a little more about how your alloc works, and which 
information it needs.

Brandon
________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Daniele Filaretti 
[dfilaretti AT gmail.com]
Sent: Tuesday, July 08, 2014 10:30 AM
To: 
k-user AT cs.uiuc.edu
Subject: [K-user] matching entire configuration while also matching its 
components

Hi All,
little technical question, in an IMP++ setting (actually only IMP, but with 
environment + store).

The following is a variable assignment rule that, in case the variable 
doesn’t exists, it creates it. In order to do this, it does the standard 
things - adding an entry in the environment and in the store, using a fresh 
allocated address.

However, I’m not using K’s builtin “fresh” predicate but I’d like to use my 
own allocation function “alloc” which takes the whole configuration as an 
input:

  rule [assign-create]:
             <k> X = I:Int; => . ... </k>
             <env> M:Map => M[alloc(State)/X] </env>
             <store> ... . => alloc(State) |-> I ... </store>
             <nextAddr> I:Int => I +Int 1 </nextAddr>)
         when notBool (X in keys(M))

As you can see, I use “alloc(State)”, where I would like “State” to match the 
entire configuration. Is that even possible?
I’ve tried with

  rule [assign-create]:
             State:Bag(
                        <k> X = I:Int; => . ... </k>
                        <env> M:Map => M[alloc(State)/X] </env>
                        <store> ... . => alloc(State) |-> I ... </store>
                        <nextAddr> I:Int => I +Int 1 </nextAddr>)
                )
         when notBool (X in keys(M))

but in this case “State” matches the empty bag (I guess) as it’s parsed as 
(Config1 Config2). Is there a way to match entire configuration (simply “give 
it a name”) and at the same time, match part of its content - all in one rule?

Thank you very much!

Regards,

Daniele
_______________________________________________
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

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