rio-maude-tutorial

Informations

• Publié par: Onfo
• Nombre de lectures: 82
• Langue: English

Extrait

Maude Introduction Course
¨
Peter C. Olveczky
University of Illinois at Urbana-Champaign
and
University of Oslo
June 1, 2004 SBLP’04 1Starting
Maude system, manual, papers, etc. at
http://maude.cs.uiuc.edu
Start Maude by giving commandmaude
Maude modules and commands can be entered at Maude command
line, or . . .
. . . can write modules and/or commands in a file and either start
Maude withmaude file.maude or by giving Maude command
in file.maude
Commandq (uit) exits a Maude session
June 1, 2004 SBLP’04 2Part 1. Equational Specifications
June 1, 2004 SBLP’04 3Functional Modules
Data type: elements + operations on these elements
Have to explicitly define all the “values” (“elements”) in the data type
The “values/elements” are terms constructed by user-defined function
symbols (operators) and constants
Terms/functions have sorts (corresponding to “data types”)
Some function symbols/constants are used to construct the
elements/values
– they are constructors
Other functions are defined functions and must be defined by
equations
General: can define all kinds of data types
June 1, 2004 SBLP’04 4Example: Natural Numbers
Equational specifications are defined as functional modules:
We define a data type of natural numbers
The numbers can represented as0,s(0),s(s(0)), . . .
One defined function_+_
fmod MY-NAT is
sort Nat .
op 0 : -> Nat [ctor] .
op s : Nat -> Nat [ctor] .
op _+_ : Nat Nat -> Nat .
vars M N : Nat .
eq 0 + M = M .
eq s(M) + N = s(M + N) .
endfm
June 1, 2004 SBLP’04 5Example: Natural Numbers (cont.)
Underscore (_) means argument position
– can write0,s(0), ands(0) + s(s(0))
Maude’sred(uce) command computes the “value” of a term by using
the equations from left to right until no equational can be applied:
Maude>red s(0) + s(s(0)) .
June 1, 2004 SBLP’04 6The Equations
The equations should be
terminating: no infinite computation possible
confluent: same result no matter how/which equations are applied
“complete”: each ground term should be reducible to a constructor
term
– make sure that a defined function is defined for all constructor
terms
June 1, 2004 SBLP’04 7Exercises I
Extend the moduleMY-NAT with functions
– _*_ for multiplication
– _! for factorial
and use Maude to compute
– (s(0) + s(0)) * (s(s(s(0))) * s(s(0)))
– (s(s(0)) * s(s(0))) !
Note: A previously defined module can be imported using
protecting orincluding:
fmod EXERCISE-1 is including MY-NAT .
...
endfm
June 1, 2004 SBLP’04 8Built-in Modules
Efficient built-in modulesNAT,INT,RAT, andSTRING
– moduleBOOL with sortBool and valuestrue andfalse,
and functionsnot,and andor, and . . . automatically imported
– Built-in modules in fileprelude.maude
Built-in functionif_then_else_fi for each sort
conditional equations written
ceq min(M, N) = M if M <= N .
June 1, 2004 SBLP’04 9Lists of Natural Numbers I
We define sortList of lists of natural numbers:
constructorsnil and_++_ (append)
one defined symbollength:
fmod LIST1 is protecting NAT .
sort List .
op nil : -> List [ctor] .
op _++_ : List Nat -> List [ctor] .
op length : List -> Nat .
var L : List . var N : Nat .
eq length(nil) = 0 .
eq length(L ++ N) = 1 + length(L) .
endfm
June 1, 2004 SBLP’04 10