Maude-help mailing list

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

Dear Bartosz, dear Paco,

@Bartosz: thanks for the reply. As I had written in my original email, I
did switch to a representation with classes/objects. My concern was not
so much whether this would be the "Maudonic" or "Maudistic" ;-) way to
capture the concept, but I was exploring the message language feature.

@Paco: ¡Muchísimas Gracias! I doubt that I would have found that one
myself anytime soon.

Best regards,

Marko


Paco Durán 
<duran AT lcc.uma.es>
 writes:

> Hi Marko, and Bartosz,
>
> Thanks, Bartosz, for your answer. However, I believe the problem is 
> somewhere else. One can use messages in any way one finds convenient. Marko 
> was not trying to transform messages into Objects. One can have a hierarchy 
> of messages Limit-Order < Order < Msg, no problem about that. I'm not going 
> into whether it makes sense or not to have such hierarchy, or whether any 
> of you had objects in mind. As I understand the spec was trying to keep 
> them as messages. 
>
> It is just a syntactic problem. Due to a wrong specification. Full Maude is 
> not very good at providing error messages, something that must be improved. 
> But the issue here is hidden by the fact that there are error messages than 
> do not show up until some term is parsed. In your spec everything is parsed 
> in a first shot (no eqs, no rls, no id elements, ...), and the module is 
> not used for parsing until the red command is entered. Therefore, the error 
> message is not about the term to be reduced, but actually, in this case, 
> for the above reason, about the spec itself. Specifically, the sort Float 
> is used without importing FLOAT. 
>
> You can find the modified modules below. 
>
> Cheers, 
>
> Paco
>
>
> (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)
>
> (omod LIMIT-ORDER is
>     protecting TRADE-ORDER .
>     pr FLOAT .
>     sort Limit-Order .
>     subsort Limit-Order < Order .
>     msg _at_ : Order Float -> Limit-Order .
> endom)
>
> (red in LIMIT-ORDER : buy 5 of "T" for "C" at 1.2 .)
>
>> On 9 Jun 2021, at 18:07, Bartosz Zieliński 
>> <bartosz.zielinski AT uni.lodz.pl>
>>  wrote:
>> 
>> 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
>

-- 
Prof. Dr. Marko Schütz-Schmuck
Department of Computer Science and Engineering
University of Puerto Rico at Mayagüez
Mayagüez, PR 00681

Attachment: signature.asc
Description: PGP signature