A Gentle Introduction to Casl

A Gentle Introduction to Casl

Documents
46 pages
Lire
Le téléchargement nécessite un accès à la bibliothèque YouScribe
Tout savoir sur nos offres

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

Informations

Publié par
Nombre de visites sur la page 121
Langue English
Signaler un problème
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
äCopyrightc2000, 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, CoFIc Michel2
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, CoFIc Michel
3
Introduction
 Bidoit, Peter D. Mosses, CoFIc 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.
cMichel Bidoit, Peter D. Mosses, CoFI
5
Underlying Concepts
Casl Tutorial
äCaslis based on standard concepts of algebraic specification.
 Bidoit, Peter D. Mosses, CoFIc Michel6
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.
cMichel Bidoit, Peter D. Mosses, CoFI
7
Loose Specifications
cMichel 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<yy<zx<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 thenx,y:Elemx<yy<xx=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%LATEXspecPartial Order= Strict Partial Order then pred(x,y:Elem)(x<yx=y) end
cMichel Bidoit, Peter D. Mosses, CoFI10
Casl Tutorial
äThe%impliesannotation is used to indicate that some axioms are supposed to be consequences of others.
specPartial Order 1= Partial Order then%implies x,y,z:Elemxyyzxz%(transitive)% end
 Bidoit, Peter D. Mosses, CoFIc Michel11
Casl Tutorial
äAttributes may be used to abbreviate axioms for associativity, commutativity, idempotence, and unit properties.
specMonoid= sortMonoid ops1:Monoid; :Monoid×MonoidMonoid,assoc,unit 1 end
cMichel Bidoit, Peter D. Mosses, CoFI12
Casl Tutorial
äGenericity of specifications can be made explicit using parameters.
specGeneric Monoid[sortElem] = sortMonoid opsinj:ElemMonoid; 1:Monoid; :Monoid×MonoidMonoid,assoc,unit 1 x,y:Eleminj(x) =inj(y)x=y
end
cMichel Bidoit, Peter D. Mosses, CoFI13
Casl Tutorial
äReferences to generic specifications always instantiate the parameters.
specGeneric Commutative Monoid[sortElem] = Generic Monoid[sortElem] thenx,y:Monoidxy=yx end specGeneric Commutative Monoid 1[sortElem] = Generic Monoid[sortElem] then op:Monoid×MonoidMonoid,comm end
 Bidoit, Peter D. Mosses, CoFIc Michel14
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,e0:Elem;C:Container • ¬(e is in empty) e is in insert(e0,C)(e=e0e 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,e0:Elem;C:Container e is in mark insert(e0,C)(e=e0e is in C) • ¬( emptye is marked in)  inserte is marked in(e0,C)e is marked in C  insert marke is marked in(e0,C)(e=e0e is marked C in) end
cMichel Bidoit, Peter D. Mosses, CoFI16
Casl Tutorial
Casl Tutorial
Generated Specifications
 Bidoit, Peter D. Mosses, CoFIc 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,e0:Elem;C:Container • ¬(e is in empty) e is in insert(e0,C)(e=e0e is in C) end
cMichel Bidoit, Peter D. Mosses, CoFI18
Casl Tutorial
äGenerated specifications are in general loose.
specGenerated Container Merge[sortElem] = Generated Container[sortElem] then opmerge:Container×ContainerContainer e:Elem;C,C0:Container e is in(C merge C0)(e is in Ce is in C0) end
cMichel 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×SetSet; remove:Elem×SetSet e,e0:Elem;S,S0:Set • ¬(e is in empty) e is in insert(e0,S)(e=e0e is in S) S=S0(x:Elemx is in Sx is in S0) e is in(SS0)(e is in Se is in S0) e is in remove(e0,S)(¬(e=e0)e is in S) then %implies generated typeSet::=empty }| {(Elem)| ∪(Set;Set) op:Set×SetSet,assoc,comm,idem,unit empty e,e0:Elem;S:Set insert(e,insert(e,S)) =insert(e,S) insert(e,insert(e0,S)) =insert(e0,insert(e,S)) end  Bidoit, Peter D. Mosses, CoFIc Michel20
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)
cMichel Bidoit, Peter D. Mosses, CoFI
21
Free Specifications
cMichel Bidoit, Peter D. Mosses, CoFI
22
Casl Tutorial
Casl Tutorial