K-user mailing list

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

Here is some more info (can you add it as well to that file, Traian?):

The best way to understand these is to forget about the Maude backend.  They 
translate the same way in Maude because Maude does nor provide us with the 
subtle differences that we need here.

macro: yes, they are supposed to apply statically, before any rewriting 
starts, both on the program and on the semantic rules.  So in terms of 
performance, they are supposed to not count (i.e., their amortized cost is 
zero).

function: is a label has this attribute, then it is as if it is a builtin 
function, the only difference being that it is "implemented" using K rules.  
We even considered changing the language in which functions are implemented, 
and following a functional style instead.  So they are meant to be very fast, 
almost instantaneous, when compared to the other rules.  Different backends 
are free to implement the functions different ways.  The symbolic execution 
engine also considers than as part of the axiomatization of the underlying 
domain in which semantic rules are applied.  So mathematically speaking, 
functions do not count as semantic computational steps.

anywhere: these are just rules which can apply anywhere they match, so they 
are expected to be comparatively very slow.  Their application counts as 
computational steps, so they are interleaved etc. in formal analyses.  It is 
hard to reason with them in reachability logic.  One should avoid such rules 
by any means if possible, and use strictness and normal rules instead.

Grigore



________________________________________
From: 
k-user-bounces AT cs.uiuc.edu
 
[k-user-bounces AT cs.uiuc.edu]
 on behalf of Michael D. Adams 
[adamsmd AT illinois.edu]
Sent: Friday, December 27, 2013 8:54 PM
To: 
k-user AT cs.uiuc.edu
Subject: Re: [K-user] Difference between 'macro', 'anywhere', and 'function'?

Does desugaring also apply to rules?  (I suspect that this could be a
major difference between 'macro' and the others.)

I don't understand what you are saying about 'function' and 'anywhere'.
  Is there any (current or planed for the future) difference in their
behavior?

(Saying that 'function' is for functions and 'anywhere' applies anywhere
doesn't help since we may have different understandings of what being a
function and applying anywhere mean.)  An example showing how they
behave differently might be enlightening.

Michael

On 12/25/2013 02:24 PM, Traian Florin Șerbănuță wrote:
> They all generate the same code now.  However, they are semantically
> different:
>
> macro should only be used for desugaring, and should be applied to
> programs before any evaluation is started.
>
> function should only be used for annotating function declarations
>
> anywhere should be used for rules which we want to apply anywhere,
> disabling configuration concretization for them.
>
> best wishes,
> Traian
>
> anywhere is
>
>
> 2013/12/25 Park, Daejun 
> <dpark69 AT illinois.edu
>  
> <mailto:dpark69 AT illinois.edu>>
>
>     Hi,
>
>     I have a simple question:
>     What is the difference between 'macro', 'anywhere', and 'function'?
>     The generated maude code seems to be same except metadata. Who
>     makes, if any, a difference?
>
>     Thanks,
>     Daejun
>     _______________________________________________
>     k-user mailing list
>     
> k-user AT cs.uiuc.edu
>  
> <mailto: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-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user