Maude-help mailing list

[Bartosz Zieliński <bartosz.zielinski AT uni.lodz.pl>]

I believe this is a slight misunderstanding of how objects are supposed to work in Maude.

Messages to not return objects (you really shouldn't do the subsort 

Order < Msg since messeges and objects are instances of common sort configuration.

Also Order should not be a sort but a class. To have objects you have to declare class and then you can construct objects with syntax < Oid : Class | Attributes >. Messages and objects are put in the commutative associative soup constructed with __  and you have rewrite rules which take 

messages and objects and return other messages and objects. Incidentally, Full Maude assumes that the first argument of the message is an Oid (object id). So a rule like 

rl < X : Counter | val : Y > inc(X) => < X : Counter | val : Y + 1 > .

defines a message (method) of the Counter class which increases value of the attribute val of objects of this class, object identifiers correlate concrete objects identified with Oid's (like references in Java) with messages.

So the whole code below (including TRADE-ORDER) makes no sense.

I would rewrite TRADE-ORDER as (I did not test it) as

(omod TRADE-ORDER is
    protecting STRING .
    protecting NAT .

    protecting QID.
    sorts Symbol CustomerId .

    subsort Qid < Oid .
    class Order | amount : Int, product: Symbol, customer: CustomerId .
endom)

and then you have order objects like < 'A : Order | amount : 10, product : ...... >.

Best regards 

Bartosz Zielinski

---

Od: Marko Schuetz-Schmuck
Wysłano: ¦roda, 09 Czerwiec 2021 17:24
Do: maude-help AT lists.cs.illinois.edu
Temat: [[maude-help] ] extending message "format"

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