Skip to Content.
Sympa Menu

maude-help - Re: [Maude-help] CRCHC Checker, prelude and owise

maude-help AT lists.cs.illinois.edu

Subject: Maude-help mailing list

List archive

Re: [Maude-help] CRCHC Checker, prelude and owise


Chronological Thread 
  • From: Francisco Durán <duran AT lcc.uma.es>
  • To: Emmanuel Castro <emmanuel.castro AT laposte.net>
  • Cc: maude-help <maude-help AT cs.uiuc.edu>
  • Subject: Re: [Maude-help] CRCHC Checker, prelude and owise
  • Date: Fri, 3 Sep 2010 12:09:08 +0200
  • List-archive: <http://lists.cs.uiuc.edu/pipermail/maude-help>
  • List-id: <maude-help.cs.uiuc.edu>

Hi Emmanuel,

As far as I know there is only  a first attempt by Steven Eker to produce a specification of the number hierarchy built-ins. It was at some point distributed as part of one of the Maude alphas

http://www.csl.sri.com/~eker/Maude/Alpha86c/numberHierachy.maude

I don't know of any attempt of generating a transformation to eliminate owises. 

Francisco


El 24/08/2010, a las 21:51, Emmanuel Castro escribió:

It is written black on white in the docs that CRCHC does not work with
built-in operation.
Does someone has written an built-in-less (non operational) equivalent
of the modules in the prelude, so that one can check the confluence of
modules protecting Nat, Qid, List...?

CRCHC does not support [owise] either.
Does someone has ever written a transformation changing an
[owise]-enabled module to an equivalent [owise]-less module, at least
when one does not use the strategy attribute.

Thank you

Emmanuel
_______________________________________________
Maude-help mailing list
Maude-help AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/maude-help




Archive powered by MHonArc 2.6.16.

Top of Page