rio-maude-tutorial

Maude Introduction Course¨Peter C. OlveczkyUniversity of Illinois at Urbana-ChampaignandUniversity of OsloJune 1, 2004 SBLP’04 1StartingMaude system, manual, papers, etc. athttp://maude.cs.uiuc.eduStart Maude by giving commandmaudeMaude modules and commands can be entered at Maude commandline, or . . .. . . can write modules and/or commands in a file and either startMaude withmaude file.maude or by giving Maude commandin file.maudeCommandq (uit) exits a Maude sessionJune 1, 2004 SBLP’04 2Part 1. Equational SpecificationsJune 1, 2004 SBLP’04 3Functional ModulesData type: elements + operations on these elementsHave to explicitly define all the “values” (“elements”) in the data typeThe “values/elements” are terms constructed by user-defined functionsymbols (operators) and constantsTerms/functions have sorts (corresponding to “data types”)Some function symbols/constants are used to construct theelements/values– they are constructorsOther functions are defined functions and must be defined byequationsGeneral: can define all kinds of data typesJune 1, 2004 SBLP’04 4Example: Natural NumbersEquational specifications are defined as functional modules:We define a data type of natural numbersThe numbers can represented as0,s(0),s(s(0)), . . .One defined function_+_fmod MY-NAT issort 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) .endfmJune 1, 2004 SBLP’04 ...