A Gentle Introduction to Casl

Description

A Gentle Introduction to Casl
Michel Bidoit
LSV, CNRS & ENS de Cachan, France
CoFI Methodology Coordinator
Peter D. Mosses
BRICS & University of Aarhus, Denmark
CoFI External Relations Coordinator
c Michel Bidoit, Peter D. Mosses, CoFI 1 Casl Tutorial
Copyright c 2000, 2001 Michel Bidoit and Peter D. Mosses,
CoFI, The Common Framework Initiative for Algebraic Speci cation
and Development.
Permission is granted to anyone to make or distribute verbatim copies of
this document, in any medium, provided that the copyright notice and
permission notice are preserved, and that the distributor grants the
recipient permission for further redistribution as permitted by this notice.
Modi ed versions may not be made.
March 25, 2001
c Michel Bidoit, Peter D. Mosses, CoFI 2 Casl TutorialContents
Introduction.........................................................4
Underlying Concepts.................................................6
Total, Many-Sorted Speci cations ....................................7
Loose Speci cations .............................................8
Generated Speci cations ........................................17
Free Speci cations .............................................22
Partial Functions ...................................................38
Subsorting .........................................................57
Structuring Speci cations ...........................................70
Generic Speci cations .............................................. ...

Sujets

• Complejo Astronómico El Leoncito
• Tutoriel
• Succieu
• Spécification fonctionnelle
• Opsimathie
• Éléments du groupe 6

Informations

• Publié par: Thoek
• Nombre de lectures: 121
• Langue: English

Extrait

A Gentle Introduction toCasl

Michel Bidoit LSV, CNRS & ENS de Cachan, France CoFIMethodology Coordinator Peter D. Mosses BRICS & University of Aarhus, Denmark CoFIExternal Relations Coordinator

 c Michel  Bidoit, Peter D. Mosses, CoFI1

Casl Tutorial

äCopyright c 2000, 2001 Michel Bidoit and Peter D. Mosses, CoFIThe Common Framework Initiative for Algebraic Specification, and Development.

Permission is granted to anyone to make or distribute verbatim copies of this document, in any medium, provided that the copyright notice and permission notice are preserved, and that the distributor grants the recipient permission for further redistribution as permitted by this notice. Modified versions may not be made.

March 25, 2001

 Bidoit, Peter D. Mosses, CoFI c Michel 2

Casl Tutorial

Contents Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 Underlying Concepts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Total, Many-Sorted Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Loose Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 Generated Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Free Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Partial Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 Subsorting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 Structuring Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 Generic Specifications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 78 Specifying Architectural Structure . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 Libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91

 Bidoit, Peter D. Mosses, CoFI c Michel

3

Introduction

 Bidoit, Peter D. Mosses, CoFI c Michel

4

Casl Tutorial

Casl Tutorial

CoFI äCoFIis an initiative to provide a common framework for algebraic specification and development. Casl äCaslhas been designed byCoFIas a general-purpose algebraic specification language, subsuming many existing languages. About This Tutorial äThis tutorial illustrates and discusses how to writeCasl specifications.

c Michel Bidoit, Peter D. Mosses, CoFI

5

Underlying Concepts

Casl Tutorial

äCaslis based on standard concepts of algebraic specification.

 Bidoit, Peter D. Mosses, CoFI c Michel 6

Casl Tutorial

Total, Many-Sorted Specifications

äTotal, many-sorted specifications inCaslmay be written essentially as in many other algebraic specification languages.

äCaslprovides also useful abbreviations.

äCaslallows loose, generated and free specifications.

c Michel Bidoit, Peter D. Mosses, CoFI

7

Loose Specifications

c Michel Bidoit, Peter D. Mosses, CoFI

8

Casl Tutorial

Casl Tutorial

äCaslsyntax for declarations and axioms involves familiar notation, and is mostly self-explanatory.

specStrict Partial Order= %%Let’s start with a simple example ! sortElem pred<:Elem×Elem %% predabbreviates predicate ∀x,y,z:Elem • ¬ (x<x) %(strict)% •x<y ⇒ ¬ (y<x) %(asymmetric)% •x<y∧y<z⇒x<z %(transitive)% %{Note that there may existx, ysuch that neitherx < ynory < x.}% end

 c Michel  Bidoit, Peter D. Mosses, CoFI9

Casl Tutorial

äSpecifications can easily be extended by new declarations and axioms.

specTotal Order= Strict Partial Order then∀x,y:Elem•x<y∨y<x∨x=y %(total)% opsmin(x,y:Elem) :Elem= xx when<y else y; max(x,y:Elem) :Elem=y when min(x,y) =x else x end

%displayleq%LATEX≤ specPartial Order= Strict Partial Order then pred≤(x,y:Elem)⇔(x<y∨x=y) end

c Michel Bidoit, Peter D. Mosses, CoFI10

Casl Tutorial

äThe %implies annotation is used to indicate that some axioms are supposed to be consequences of others.

specPartial Order 1= Partial Order then %implies ∀x,y,z:Elem•x≤y∧y≤z⇒x≤z %(transitive)% end

 Bidoit, Peter D. Mosses, CoFI c Michel 11

Casl Tutorial

äAttributes may be used to abbreviate axioms for associativity, commutativity, idempotence, and unit properties.

specMonoid= sortMonoid ops1:Monoid; ∗:Monoid×Monoid→Monoid,assoc,unit 1 end

c Michel Bidoit, Peter D. Mosses, CoFI12

Casl Tutorial

äGenericity of specifications can be made explicit using parameters.

specGeneric Monoid[sortElem] = sortMonoid opsinj:Elem→Monoid; 1:Monoid; ∗:Monoid×Monoid→Monoid,assoc,unit 1 ∀x,y:Elem•inj(x) =inj(y)⇒x=y

end

c Michel Bidoit, Peter D. Mosses, CoFI13

Casl Tutorial

äReferences to generic specifications always instantiate the parameters.

specGeneric Commutative Monoid[sortElem] = Generic Monoid[sortElem] then∀x,y:Monoid•x∗y=y∗x end specGeneric Commutative Monoid 1[sortElem] = Generic Monoid[sortElem] then op∗:Monoid×Monoid→Monoid,comm end

 Bidoit, Peter D. Mosses, CoFI c Michel 14

Casl Tutorial

äDatatype declarations may be used to abbreviate declarations of sorts and constructors.

specContainer[sortElem] = typeContainer::=empty|insert(Elem;Container) predis in:Elem×Container ∀e,e 0 :Elem;C:Container • ¬ (e is in empty) •e is in insert(e 0 ,C)⇔(e=e 0 ∨e is in C) end

 c Michel  Bidoit, Peter D. Mosses, CoFI15

äLoose datatype declarations are appropriate when further constructors may be added in extensions.

specMarking Container[sortElem] = Container[sortElem] then typeContainer::=mark insert(Elem;Container) predis marked in:Elem×Container ∀e,e 0 :Elem;C:Container •e is in mark insert(e 0 ,C)⇔(e=e 0 ∨e is in C) • ¬ ( emptye is marked in) • inserte is marked in(e 0 ,C)⇔e is marked in C • insert marke is marked in(e 0 ,C)⇔ (e=e 0 ∨e is marked C in) end

c Michel Bidoit, Peter D. Mosses, CoFI16

Casl Tutorial

Casl Tutorial

Generated Specifications

 Bidoit, Peter D. Mosses, CoFI c Michel

17

äSorts may be specified as generated by their constructors.

Casl Tutorial

specGenerated Container[sortElem] = generated typeContainer::=empty|insert(Elem;Container) predis in:Elem×Container ∀e,e 0 :Elem;C:Container • ¬ (e is in empty) •e is in insert(e 0 ,C)⇔(e=e 0 ∨e is in C) end

c Michel Bidoit, Peter D. Mosses, CoFI18

Casl Tutorial

äGenerated specifications are in general loose.

specGenerated Container Merge[sortElem] = Generated Container[sortElem] then opmerge:Container×Container→Container ∀e:Elem;C,C 0 :Container •e is in(C merge C 0 )⇔(e is in C∨e is in C 0 ) end

c Michel Bidoit, Peter D. Mosses, CoFI19

äGenerated specifications need not be loose. specGenerated Set[sortElem] = generated typeSet::=empty|insert(Elem;Set) predis in:Elem×Set ops{ }(e:Elem) :Set=insert(e,empty); ∪:Set×Set→Set; remove:Elem×Set→Set ∀e,e 0 :Elem;S,S 0 :Set • ¬ (e is in empty) •e is in insert(e 0 ,S)⇔(e=e 0 ∨e is in S) •S=S 0 ⇔(∀x:Elem•x is in S⇔x is in S 0 ) •e is in(S∪S 0 )⇔(e is in S∨e is in S 0 ) •e is in remove(e 0 ,S)⇔( ¬ (e=e 0 )∧e is in S) then %implies generated typeSet::=empty }| {(Elem)| ∪(Set;Set) op∪:Set×Set→Set,assoc,comm,idem,unit empty ∀e,e 0 :Elem;S:Set •insert(e,insert(e,S)) =insert(e,S) •insert(e,insert(e 0 ,S)) =insert(e 0 ,insert(e,S)) end  Bidoit, Peter D. Mosses, CoFI c Michel 20

Casl Tutorial

Casl Tutorial

äGenerated types may need to be declared together.

sortNode generated typeTree::=mktree(Node;Forest) generated typeForest::=empty|add(Tree;Forest)

is bothincorrect(linear visibility) andwrong(the corresponding semantics is not the “expected” one). One must write instead:

sortNode generated typesTree::=mktree(Node;Forest); Forest::=empty|add(Tree;Forest)

c Michel Bidoit, Peter D. Mosses, CoFI

21

Free Specifications

c Michel Bidoit, Peter D. Mosses, CoFI

22

Casl Tutorial

Casl Tutorial