K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

The [owise] attribute is currently supported only on function rules. It's possible, depending on the order rules are chosen for evaluation, that during concrete execution a non-function rule tagged with owise may appear to behave correctly. However, this is an artifact of the order rules are chosen for evaluation in, and the rules are actually forming a critical pair.

Eventually the plan is to have a way of specifying rewrite strategies that will allow more complete behaviors like this, but that functionality is not yet supported.

On Tue, Feb 17, 2015 at 8:48 PM, Mark Hills <markhills1 AT gmail.com> wrote:

I'm currently creating some rules for processing terms in the LAMBDA tutorial example and am using [owise] on a couple of the rules that handle default cases. I'm just checking to see what the current status of [owise] is, since I thought at some point it wasn't supported, or was only supported on operators marked as [function], but in my case I'm using it with normal K rules and it seems to work fine. It could also be that there is some good way to handle default cases that doesn't use [owise], in which case I would be happy to hear about it.

Best regards,

Mark

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