Formal Methods Forumにて、MAUDE 2.0 Primerを輪読中。
fmod AUTHOR is
protecting STRING .
sort CatalogCard .
sorts Name Title PublDate Location .
subsort String < Name .
subsort String < Title .
subsort String < PublDate .
subsort String < Location .
op n_t_pd_l_ : Name Title PublDate Location -> CatalogCard [ctor] .
op author : CatalogCard -> Name .
eq author(n N:Name t T:Title pd P:PublDate l L:Location) = N:Name .
endfm
*** reduce author(n "ken" t "java" pd "2012" l "japan") .
fmod PEANO-NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
endfm
fmod PEANO-NAT-EXTRA is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor iter] .
op _+_ : Nat Nat -> Nat .
op _-_ : Nat Nat -> Nat .
vars M N : Nat .
eq 0 + N = N .
eq s(M) + N = s(M + N) .
eq N - 0 = N .
eq 0 - N = 0 .
eq s(N) - s(M) = N - M .
endfm
fmod PEANO-NAT-MULT is
protecting PEANO-NAT-EXTRA .
op _*_ : Nat Nat -> Nat .
vars M N : Nat .
eq N * 0 = 0 .
eq N * s(M) = N + (N * M) .
endfm
*** reduce s^3(0) * s^5(0) .
fmod LIST is
protecting PEANO-NAT-EXTRA .
sorts Elt List .
subsort Nat < Elt < List .
op nil : -> List [ctor] .
op __ : List List -> List [ctor assoc id: nil] .
endfm
fmod LIST-SIZE is
protecting LIST .
protecting PEANO-NAT-EXTRA .
op size : List -> Nat .
var E : Elt .
var L : List .
eq size(nil) = 0 .
eq size(E L) = s(size(L)) .
endfm
*** reduce size(0 0 0 0) .
fmod CARD-DECK is
sorts Number Suit Card .
ops A 2 3 4 5 6 7 8 9 10 J Q K : -> Number [ctor] .
ops Clubs Diamonds Hearts Spades : -> Suit [ctor] .
op _of_ : Number Suit -> Card [ctor] .
op CardNum : Card -> Number .
op CardSuit : Card -> Suit .
var N : Number .
var S : Suit .
eq CardNum(N of S) = N .
eq CardSuit(N of S) = S .
endfm
fmod NAT-BOOL is
protecting PEANO-NAT-EXTRA .
op _<=_ : Nat Nat -> Bool .
op _>_ : Nat Nat -> Bool .
vars M N : Nat .
eq 0 <= N = true .
eq s(M) <= 0 = false .
eq s(M) <= s(N) = M <= N .
eq M > N = not(M <= N) .
ceq N - M = 0 if M > N .
endfm
fmod IRRITABLE-PROFESSOR is
protecting STRING .
sorts Question Exclamation Interruption .
subsorts Question Exclamation < Interruption .
op _? : String -> Question [ctor] .
op _! : String -> Exclamation [ctor] .
op reply : Interruption -> String .
var I : Interruption .
ceq reply(I) = "Questions after class, please" if (S:String) ? := I .
endfm
fmod CRAZY-EIGHTS is
protecting CARD-DECK .
sort WildCard .
subsort WildCard < Card .
var C : Card .
cmb C : WildCard if CardNum(C) == 8 .
endfm
*** Maude> reduce in CRAZY-EIGHTS : 8 of Clubs .
*** reduce in CRAZY-EIGHTS : 8 of Clubs .
*** rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
*** result WildCard: 8 of Clubs
*** Maude> reduce in CRAZY-EIGHTS : 9 of Clubs .
*** reduce in CRAZY-EIGHTS : 9 of Clubs .
*** rewrites: 2 in 0ms cpu (0ms real) (~ rewrites/second)
*** result Card: 9 of Clubs
*** Maude>
fmod SUICIDE-KING is
protecting CARD-DECK .
sort SuicideKing .
subsort SuicideKing < Card .
mb K of Hearts : SuicideKing .
endfm
*** Maude> reduce in SUICIDE-KING : K of Hearts .
*** reduce in SUICIDE-KING : K of Hearts .
*** rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
*** result SuicideKing: K of Hearts
*** Maude> reduce in SUICIDE-KING : K of Clubs .
*** reduce in SUICIDE-KING : K of Clubs .
*** rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
*** result Card: K of Clubs
*** Maude>
fmod CARD-PAIR is
protecting CARD-DECK .
sorts Pair PokerPair .
subsort PokerPair < Pair .
op <_;_> : Card Card -> Pair [ctor comm] .
var N : Number .
var P : Pair .
cmb P : PokerPair if < N of S:Suit ; N of S':Suit > := P .
endfm
*** Maude> reduce in CARD-PAIR : < 8 of Clubs ; 8 of Hearts > .
*** reduce in CARD-PAIR : < 8 of Clubs ; 8 of Hearts > .
*** rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
*** result PokerPair: < 8 of Clubs ; 8 of Hearts >
*** Maude> reduce in CARD-PAIR : < 8 of Clubs ; 9 of Hearts > .
*** reduce in CARD-PAIR : < 8 of Clubs ; 9 of Hearts > .
*** rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
*** result Pair: < 8 of Clubs ; 9 of Hearts >
fmod DOG-RACING is
protecting DOGS .
protecting NAT .
op race : Dog Dog -> Dog .
op speed : Dog -> Nat .
vars N M : Dog .
eq speed(bloodhound) = 20 .
eq speed(collie) = 25 .
eq speed(frog) = 5 .
eq speed(breed(N, M)) = (speed(N) + speed(M)) quo 2 .
ceq race(N, M) = N if speed(N) > speed(M) .
eq race(N, M) = M [owise] .
endfm
