Maude-Schnelleinstieg

Maude ist eine Spezifikationssprache, die auf Rewriting Logic basiert. Spezifikationen in Maude schreiben f�hlt sich aber sehr wie funktionales Programmieren an, so dass es Ihnen sicher hilft, wenn Sie sich an ML zur�ckerinnern.

Download, Installation, Dokumentation

Auf der Maude Website:

Maude Primer: Sehr lesbares Tutorial f�r Maude.
Maude Manual: Ausf�hrliches, klar strukturiertes Handbuch; zum Nachschlagen von Modulen etc.
Download and Installation: Maude gibt es f�r Windows, Linux und den Mac.

Verwendung des Maude-Interpreters mit den Standard-Modulen

moosach(rauschma):~/gse/maude % maude
                     \||||||||||||||||||/
                   --- Welcome to Maude ---
                     /|||||||||||||||||| Maude 2.1.1 built: Jun 15 2004 12:55:31

             Copyright 1997-2004 SRI International
                   Wed Oct 26 12:48:57 2005
Maude> select NAT .
Maude> red 3 * 77 .
reduce in NAT : 3 * 77 .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NzNat: 231
Maude> red sd(9,2) . --- symmetrische Differenz: sd(x,y) entspricht dem Absolutbetrag | x - y |
reduce in NAT : sd(2, 9) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NzNat: 7
Maude> red sd(2,9) .
reduce in NAT : sd(2, 9) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result NzNat: 7
Maude>

Hinweise zur Kommandozeile:

Zeilen werden immer durch ein Kommando eingeleitet. So kann man leider nicht einfach Ausdr�cke hinschreiben und diese reduzieren lassen, sondern muss immer ein red davor schreiben.

Ein Beispiel-Modul

...gespeichert in einer Datei "SIMPLE_LIST.maude".


mod SIMPLE_LIST is

  --- Importieren von Modulen

  protecting NAT .
  protecting STRING .
  protecting BOOL .

  sort List .

  op empty : -> List [ctor] .
  op cons : String List -> List [ctor] .
  op get : List Nat -> String .

  var I : Nat .
  var L : List .
  var S : String .

  eq get(empty, I) = "" .
  eq get(cons(S,L), 0) = S .

  --- Nat�rliche Zahlen haben kein '-' sondern nur 'sd' (symmetric difference),
  --- das die (positive) Differenz zweier Zahlen ermittelt

  ceq get(cons(S,L), I) = get(L, sd(I,1)) if I > 0 .

  --- syntactic sugar for lists

  op __ : String List -> List .
  eq S L = cons(S, L) .

endm

Grundlegende Hinweise zu Maude:

Leerzeichen spielen eine grosse Rolle. Vor allem zwischen Namen und Trennzeichen lohnt es sich, Leerzeichen zu machen, wenn einmal etwas nicht geparst werden kann.
Kommentare
Punkt am Ende jeder Zeile
Flags in Eckigen Klammern: ctor
Conditional Equations
Modul-Import
Concatenation-Operator

Beispielsitzung mit SIMPLE_LIST

Maude> load SIMPLE_LIST --- tab expansion funktioniert!
Maude> red "a" "b" "c" empty .
reduce in SIMPLE_LIST : "a" "b" "c" empty .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result List: cons("a", cons("b", cons("c", empty)))
Maude> red get("a" "b" "c" empty, 1) .
reduce in SIMPLE_LIST : get("a" "b" "c" empty, 1) .
rewrites: 7 in 0ms cpu (0ms real) (~ rewrites/second)
result Char: "b"
Maude>

Axel Rauschmayer, Last change: 2005-10-26