Maude-help mailing list

[Marko Schuetz-Schmuck <MarkoSchuetz AT web.de>]

Dear All,

I'm still very new to Maude. I ran into something that has me
puzzled. Say I define the module TRADE-ORDER: 

(omod TRADE-ORDER is
    protecting STRING .
    protecting NAT .
    sorts Order Symbol CustomerId .
    subsort Order < Msg .
    subsorts String < Symbol CustomerId .
    msg buy_of_for_ : Nat Symbol CustomerId -> Order .
    msg sell_of_for_ : Nat Symbol CustomerId -> Order .
endom)

and based on that I want to define a LIMIT-ORDER which is just a
TRADE-ORDER with a limit (of course I didn't want to duplicate the parts
of the message that are already in TRADE-ORDER). So I tried the
following (which would have some drawbacks even if it would work,
e.g. multiple nested "at"s):

(omod LIMIT-ORDER is
    protecting TRADE-ORDER .
    sort Limit-Order .
    subsort Limit-Order < Order .
    msg _at_ : Order Float -> Limit-Order .
endom)

I was expecting to be able to write

(red in LIMIT-ORDER : buy 5 of "T" for "C" at 1.2 .)

but that results in "incorrect command". I have since changed this to
objects and classes, but the syntax is not as plain as it would be with
the above.

Best regards,

Marko

Attachment: signature.asc
Description: PGP signature