Σύστημα Maude

To σύστημα Maude είναι μια υλοποίηση της λογικής επαναγραφής που αναπτύχθηκε στο SRI International. Η προσέγγισή του γενικά μοιάζει με την υλοποίηση OBJ3 της εξισωτικής λογικής (equational logic) από τον Joseph Goguen, αλλά βασίζεται στη λογική επαναγραφής αντί για την εξισωτικής λογικής με διατεταγμένους τύπους (order-sorted equational logic), με έμφαση στον ισχυρό μεταπρογραμματισμό που βασίζεται στην ανάκλαση.

Maude - τα βασικά

Οι μονάδες (modules) του Maude (θεωρίες επαναγραφής, rewrite theories) αποτελούνται από μια γλώσσα όρων και ένα σύνολο από ισότητες και κανόνες επαναγραφής. Οι όροι σε μια θεωρία επαναγραφής κατασκευάζονται με τη χρήση τελεστών ("operators"), που είναι συναρτήσεις που δέχονται 0 ή περισσότερα ορίσματα ενός τύπου (sort) και επιστρέφουν έναν όρο ενός συγκεκριμένου τύπου. Οι τελεστές που δέχονται 0 ορίσματα θεωρούνται σταθερές και η γλώσσα των όρων κατασκευάζεται από αυτές τις απλές δομές.
ΣΗΜΕΙΩΣΗ: Τα παρακάτω προγράμματα μπορούν να εκτελεστούν αν δοθεί στο Maude η επιλογή -no-prelude η οποία δεν επιτρέπει στο Maude να περιλαμβάνει τις βασικές του ενότητες (όπως την ενότητα NAT του Maude που θα προκαλούσε σύγκρουση).

Παράδειγμα 1

fmod NAT is
   sort Nat .

   op 0 : -> Nat [ctor] .
   op s : Nat -> Nat [ctor] .
 endfm
Αυτή η θεωρία επαναγραφής ορίζει όλους τους φυσικούς αριθμούς. Αρχικά εισάγεται ο τύπος, λέγοντας ότι υπάρχει ένα τέτοιο και ονομάζεται Nat (συντομογραφία για τους ακέραιους αριθμούς, αγγλ. όρος "natural numbers"), και ακολουθεί η προδιαγραφή που περιγράφει πώς κατασκευάζονται. Ο τελεστής s στο Παράδειγμα 1 είναι η συνάρτηση "επόμενο" ("successor") που αναπαριστά τον επόμενο φυσικό αριθμό στην ακολουθία των φυσικών αριθμών, δηλ. s(N) := N + 1. Ο s(0) εννοείται ότι αναπαριστά το φυσικό αριθμό 1, ακολουθούν όμοια και οι υπόλοιποι. Ο 0 είναι μια σταθερά, δε δέχεται παραμέτρους εισόδου αλλά επιστρέφει έναν Nat.

Κανόνες επαναγραφής

Αν και μέχρι τώρα η επαναγραφή και η αναγωγή χειρίστηκαν με τον ίδιο τρόπο, αυτό οφείλεται στο ότι η παραπάνω θεωρία επαναγραφής δεν είχε κανόνες επαναγραφής, αν και έγινε επαναγραφή όρων. Ακολουθεί η ανάλυση των κανόνων επαναγραφής και της διαφοράς τους από τις εξισώσεις, όπως αυτές εμφανίστηκαν παραπάνω.
Η ενότητα NAT των ακέραιων αριθμών και της πρόσθεσης, που ήδη παρουσιάστηκε, θεωρείται συναρτησιακή μονάδα (functional module) ή θεωρία επαναγραφής (rewrite theory), γιατί δεν περιέχει κανόνες επαναγραφής. Για αυτόν το λόγο, αυτές οι ενότητες συνήθως περιέχονται ανάμεσα στις λέξεις fmod και endfm (αντί για τις mod και endm). Μια συναρτησιακή μονάδα και οι εξισώσεις της πρέπει να συμβάλλουν και να τερματίζουν γιατί αποτελούν το τμήμα της θεωρίας επαναγραφής που πρέπει πάντα να υπολογίζει το ίδιο αποτέλεσμα, κάτι που θα φανεί και στη συνέχεια, από την περιγραφή της λειτουργίας των κανόνων επαναγραφής.

Παράδειγμα 3

mod PERSON is

including NAT . *** η προηγούμενη μονάδα

sort Person .
sort State .

op married : -> State [ctor] .
op divorced : -> State [ctor] .
op single : -> State [ctor] .
op engaged : -> State [ctor] .
op dead : -> State [ctor] .

op person : State Nat -> Person [ctor] .

var N : Nat .
var S : State .

rl [birthday] :

person (S, N) => person (S, N + s(0)) .

rl [get-engaged] :

person (single, N) => person (engaged, N) .

rl [get-married] :

person (engaged, N) => person (married, N) .

rl [get-divorced] :

person (married, N) => person (divorced, N) .

rl [las-vegas] :

person (S, N) => person (married, N) .

rl [die] :

person (S, N) => person (dead, N) .

endm
Αυτή η ενότητα εισάγει δύο νέους τύπους και ένα σύνολο από κανόνες επαναγραφής. Περιέχεται επίσης η προηγούμενη μονάδα, για να φανεί η διαφορά μεταξύ εξισώσεων και κανόνων επαναγραφής. Οι κανόνες επαναγραφής μπορούν να θεωρηθούν ως ένα σύνολο από επιτρεπτές αλλαγές κατάστασης και, ενώ οι εξισώσεις διατηρούν την ίδια σημασία και στα δύο μέλη του συμβόλου της ισότητας, οι κανόνες επαναγραφής δεν έχουν αυτήν την ιδιότητα (οι κανόνες επαναγραφής χρησιμοποιούν το σύμβολο => αντί του συμβόλου της ισότητας). Στο παραπάνω παράδειγμα, ένα πρόσωπο, όταν παντρεύεται, δεν αλλάζει αλλά κάτι έχει αλλάξει, τουλάχιστον η οικογενειακή κατάσταση. Αυτό φαίνεται από έναν κανόνα επαναγραφής και όχι μια εξίσωση. Οι κανόνες επαναγραφής δε χρειάζεται να συμβάλλουν και να τερματίζουν, επομένως είναι σημαντικό ποιοι κανόνες επιλέγονται για να επαναγραφεί ένας όρος. Οι κανόνες εφαρμόζονται "τυχαία" από το σύστημα Maude, δεν είναι δηλαδή σίγουρο αν κάποιος κανόνας εφαρμόζεται πριν από κάποιον άλλο, κλπ. Αν μια εξίσωση μπορεί να εφαρμοστεί σε έναν όρο, πάντα θα εφαρμόζεται πριν από κάποιον κανόνα επαναγραφής.
Ένα μικρό παράδειγμα:

Παράδειγμα 4

rewrite [3] in PERSON : person (single, 0) .

rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)

result Person: person (married, s(0))
Σε αυτό το παράδειγμα δίνεται η εντολή στο Maude να επαναγράψει τον όρο που δίνεται σύμφωνα με τη θεωρία επαναγραφής και να σταματήσει μετά από 3 βήματα επαναγραφής (ένα άνω όριο μπορεί να χρειάζεται επειδή οι κανόνες επαναγραφής δεν είναι απαραίτητο ότι τερματίζουν ή συμβάλλουν), ώστε να φανεί η τελική κατάσταση μετά από την εφαρμογή 3 τυχαία επιλεγμένων κανόνων. Το αποτέλεσμα είναι περίεργο ως έννοια (η ηλικία είναι 1) και εμφανίζει 4 βήματα επαναγραφής (επειδή τα βήματα επαναγραφής από την εφαρμογή εξισώσεων δεν υπολογίζονται, μιας και δεν αλλάζουν τον όρο αν οι εξισώσεις είναι σωστές). Σε αυτό το παράδειγμα χρησιμοποιείται μια από τις εξισώσεις της μονάδας NAT για την αναγωγή του όρου 0 + s(0) σε s(0), στην οποία οφείλεται το 4ο βήμα αναγωγής.
Για να διορθωθεί το παράδειγμα, κάποιοι κανόνες επαναγραφής μπορούν να τροποποιηθούν και να γίνουν κανόνες επαναγραφής υπό συνθήκη (conditional), που σημαίνει ότι πρέπει να ικανοποιούν κάποια επιπλέον κριτήρια (εκτός του ταιριάσματος του αριστερού τους μέλους) για να εφαρμοστούν.
crl [las-vegas] :

person (S, N) => person (married, N) if (S =/= married) /\ (S =/= dead) .

crl [die] :

person (S, N) => person (dead, N) if (S =/= dead) .
Είναι λογικό ότι ένας άνθρωπος δε μπορεί να πεθάνει αν είναι ήδη νεκρός (dead) και δε μπορεί να παντρευτεί αν είναι ήδη παντρεμένος (married). Το σύμβολο (/\) συμβολίζει το λογικό ΚΑΙ (AND) και σημαίνει ότι πρέπει να ικανοποιούνται και τα δύο επιπλέον κριτήρια για την εφαρμογή του όρου. Οι εξισώσεις μπορούν επίσης να γραφούν υπό συνθήκη με παρόμοιο τρόπο.

Λόγοι χρήσης της Λογικής Επαναγραφής και του Maude

Το Maude στοχεύει στην επίλυση διαφορετικών προβλημάτων από αυτά που χειρίζονται οι συνηθισμένες προστακτικές γλώσσες, όπως η C, η Java ή η Perl. Είναι ένα εργαλείο τυπικής συλλογιστικής που βεβαιώνει το χρήστη ότι κάποιες ιδιότητες είναι σωστές ή δείχνει γιατί αυτές δεν ισχύουν. Το Maude επιτρέπει να βρεθεί τυπικά τι σημαίνει μια ιδέα σε αφηρημένο επίπεδο (χωρίς να χρειάζονται λεπτομέρειες της υλοποίησής της), περιγράφοντας τι θεωρείται ισοδύναμο στη θεωρία (εξισώσεις) και πώς μπορεί να αλλάξει (κανόνες επαναγραφής). Αυτό αποδεικνύεται πολύ χρήσιμο στον έλεγχο της ορθότητας πρωτοκόλλων ασφαλείας και σημαντικού κώδικα. Το σύστημα Maude έχει αποδείξει σφάλματα σε πρωτόκολλα κρυπτογραφίας, απλά περιγράφοντας τις δυνατότητες του συστήματος (όπως η θεωρία επαναγραφής PERSON), και αναζητώντας μη επιθυμητές καταστάσεις (καταστάσεις ή όρους που δεν είναι επιθυμητό να μπορούν να εμφανιστούν), αποδεικνύονται τα σφάλματα του πρωτοκόλλου. Τα σφάλματα αυτά μπορούν να είναι δύσκολα στην ανίχνευση γιατί συμβολίζουν καταστάσεις εκτός του κλασικού τρόπου λειτουργίας και ο προγραμματιστής μπορεί εύκολα να μην τα έχει υπόψη του.
Το Maude περιέχει ενσωματωμένη μια μηαχνή αναζήτησης για μη επιθυμητές καταστάσεις ή μπορεί να δείξει ότι τέτοιες καταστάσεις δε μπορούν να εμφανιστούν.
Ακολουθεί άλλο ένα μικρό παράδειγμα της μονάδας PERSON.
search [1] in PERSON : person (single, 1) =>1 person (married, 2) .

No solution.
Εδώ οι φυσικοί αριθμοί ακολουθούν τον κλασικό συμβολισμό (έχει φορτωθεί η βασική μονάδα prelude.maude του Maude με την εντολή "in prelude", ή το 1 μπορεί να αντικατασταθεί από το s(0) και το 2 από το s(s(0)) αν δεν πρόκειται να φορτωθούν οι βασικές ενότητες του Maude), γενικά το Maude έχει ενσωματωμένη υποστήριξη για συνηθισμένες δομές όπως οι ακέραιοι ή οι αριθμοί κινητής υποδιαστολής. Οι φυσικοί αριθμοί εξακολουθούν να είναι μέλη του ενσωματωμένου τύπου Nat. Δηλώνεται ότι πρόκειται να γίνει αναζήτηση για μια μετάβαση που χρησιμοποιεί έναν κανόνα επαναγραφής (=>1), ο οποίος να επαναγράφει τον πρώτο όρο στον δεύτερο. Το αποτέλεσμα είναι προφανές. Αν επιτραπεί στο Maude να χρησιμοποιήσει παραπάνω από ένα βήμα, προκύπτει διαφορετικό αποτέλεσμα:
search [1] in PERSON : person (single, 1) =>+ person (married, 2) .

Solution 1 (state 7)
states: 8 rewrites: 14 in 0ms cpu (0ms real) (~ rewrites/second)
Η ενσωματωμένη εντολή show path δείχνει ποιες εφαρμογές κανόνων οδηγούν στον τελικό όρο. Το σύμβολο (=>+) σημαίνει μια ή περισσότερες εφαρμογές όρων.
show path 7 .
state 0, Person: person (single, 1)
===[[rl person(S, N) => person(S, N + 1) [label 'birthday]] .]
===>
state 1, Person: person (single, 2)
===[[crl person(S, N) => person(married, N) if S =/= married = true /\ S =/= dead = true [label las-vegas]] .]
===>
state 7, Person: person (married, 2)
Το επιθυμητό αποτέλεσμα προκύπτει από την εφαρμογή του κανόνα "birthday" και μετά του κανόνα "las-vegas". Η προσέγγιση αυτή δεν ενδείκνυται πάντα γιατί όλες οι θεωρίες επαναγραφής ή οι μονάδες με πολλές πιθανές εφαρμογές κανόνων παράγουν ένα τεράστιο δέντρο πιθανών καταστάσεων που δε μπορεί να χειριστεί από την εντολή search. Μπορεί επίσης να ελεγχθεί ποιος κανόνας μπορεί να χρησιμοποιηθεί σε κάθε βήμα, μέσω μεταπρογραμματισμού λόγω της ανακλαστικής ιδιότητας της λογικής επαναγραφής.
Το Maude είναι ελεύθερο λογισμικό και υπάρχει αρκετό εκπαιδευτικό υλικό διαθέσιμο.