K-user mailing list

[Daniele Filaretti <dfilaretti AT gmail.com>]

On 9 Jul 2014, at 13:59, Rosu, Grigore 
<grosu AT illinois.edu>
 wrote:

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

Yes, this will be a very useful feature! 
In the meanwhile I’ll use Brandon’s solution which does the job for now.
(sorry for double-reply, I sent a reply before to “k-list” but got rejected).

Thanks! 

> ________________________________________
> 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