Maude-help mailing list

[Patrick Lincoln <lincoln AT csl.sri.com>]

--- Begin Message ---

• From: megzari <karim.megzari AT univ-savoie.fr>
• To: Lincoln AT csl.sri.com
• Subject: [Maude-user] 2 questions !
• Date: Mon, 07 Jul 2003 13:57:54 +0200

Dear Patrick,

I have 2 questions related to Maude, I have Just start to learn it ! :)

a) We can for example Rewrite a module A.fm by a module B.fm (with
applying some rewriting rules that add sorts or rules, for
instance), and store the new module B.fm in the Persistent Maude
DataBase ? and show it by the command show ? otherwise, I want to refine
the
module A.fm (with a new body) ! :)

b) How we can describe or specify preconditions and postconditions in
Maude ? in semantic Level !

for instance, how we can please do this in Maude :

refine ModuleA by ModuleA1 {
precondiction ( the sort s not exist in the moduleA)
postcondition (add sort s in the moduleA)
} as ModuleA1

when we write the command Maude>Show ModuleA1
Maude output :
fmod ModuleA1 is
sort s1 .... s

Thank you,

---------------------------------------------------------------
Karim Megzari
Phd student at SEG/Listic - Annecy (France)
+33450096591
---------------------------------------------------------

--- End Message ---