Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

On Friday 08 April 2011 06:19:06 am polina delfia wrote:
> Hi, I’m new on Maude use, could u expalin to me by examples what’s the
>  differences between  the 2 operator attributes strat and owise??
> 

The strat attribute is given to _operators_. It specifies what order
the arguments are evaluated in and when should evaluation at the top
should take place. It's a hold over from OBJ3, Maude's predecessor and
it might be severely curtailed in our next rewriting engine.
It's costly (in performance and code) to implement and hardly
ever used since for confluent and terminating term rewriting, order of
evaluation should matter (except perhaps for performance).

A good example of its use is:

  op _and-then_ : Bool Bool -> Bool [strat (1 0) gather (e E) prec 55] .

in fmod EXT-BOOL, in prelude.maude

The owise attribute is given to _equations_. It allows some degree of
control over which order equations are tried - those with the
attribute are tried only after those without the attribute have
failed. It also changes the semantics of the equation - implicitly an
equation with the owise attribute becomes conditional on the
equations without owise having failed.

A good example of its use is:

  op delete : X$Elt Set{X} -> Set{X} .
  eq delete(E, (E, S)) = delete(E, S) .
  eq delete(E, S) = S [owise] .

in fmod SET{X :: TRIV}, in prelude.maude

Steven