Home

User Manual

1. 0 33 4 4 Existential equality sees 35 5 22 222 22222 2 2 4 RARE 37 5 1 Subsort Declarations and 37 5 2 Subsorts and Overloading 41 5 3 Subsorts and 42 et 47 der a eate dieat ere 47 0 2 Renaming neresen ienei e ti ea 49 6 3 cert pais RR EUR eee eas RR UR 51 6 4 Local Symbols 2 25 eR UE eae Rd 52 6 5 Named Specifications 55 X Contents EE E 57 ee eee Se a ee 58 63 7 3 Parameters with Fixed 66 TA Views ood Aas Veo 68 Feste beds stu erbe urbs cu dte 201 8 1 Architectural Specifications 203 d Pedes 206 TE 213 UT 217 9 1 Local Libraries 2255 LEE Gr Ripa Re ex 218 9 2 Distributed Libraries 0 0 0 0 00000 cee ee 223 0 3 Version control us 226 TOT E TERES 83 M M 85 10 6 Other tools 85 n 87 92 95 96
2. 134 C 6 1 Predicting the Output of Steam and the Water Level 136 C 6 2 Predicting the Pump and Pump Controller States 139 C 7 Specifying the Messages to 141 C 8 The Steam Boiler Control System 142 C 9 Validation of the CASL Requirements Specification 143 C 10 Designing the Architecture of the Steam Boiler Control System CO l1 GConcl sionp ons cR beet rer dor ep soe Eee ea one 148 148 DIEM 148 C 12 2 Physical 149 I 151 D POTES 152 Dane toa aiding a a m datas 154 baa pau aoe oad 155 p dec ut pd qd edis 156 157 Tm 165 Page XI FIRST PUBLIC DRAFT 17 8ep 2003 17 54 1 Introduction 1 1 CoFI CoFI is an initiative to provide a common framework for algebraic specification and development e Background e Aims e Status 1 2 CASL CASL has been designed by COFI as a general purpose algebraic spec ification language subsuming many existing languages e General features e Major parts e Specific features 2 Underlying Concepts 2 1 Specifications e Symbols e Declarations e Axioms e Structure e Architecture e Libraries 2 2 Algebras e Signatures e Models e Classes of models 3 Total Many Sorted Specifications Total many sorte
3. 96 98 ymmo N 99 ATA COMMENES os cc cee aded 100 A 1 5 100 CDD 101 IM II MU 101 rms 101 poc PER 101 T 102 Architectural 102 rM 102 dd send ue dc 102 sues raed Att napintas stated a das 102 A 3 4 Unit Declarations and Definitions 102 Page X FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Contents XI ee 102 Tercera er meee EE 102 pum 103 NONEM 103 4 2 T 105 B 1 Library Basic Numbers 105 108 115 115 2 Getting Sbarted 4er Ce 117 snb e vire bees outer reet 120 128 126 C 5 1 Understanding the Detection of Equipment Failures 126 C 5 2 Keeping Track of the Status of the Physical Units C 5 3 Detection of the Message Transmission System Failures C 5 4 Detection of the Pump and Pump Controller Failures 131 C 5 5 Detection of the Steam and Water Level Measurement 133 5 6 arini ER eee diss tive sweated 134 C 6 Predicting the Behaviour of the Steam Boiler
4. Vb e 9696 abbreviates SYi SYi A 3 Architectural Specifications A 3 1 Named Specifications arch spec ASN ASP end named arch spec unit spec SN USP end named unit spec A 3 2 Architectural Specifications ASP ASN arch spec name units UD1 UDn result UE basic arch spec A 3 3 Unit Specifications USP SP unit type SP1 x x SPnto SP functional unit type closed USP 9696 non extension arch spec ASP 9696 models of arch spec A 3 4 Unit Declarations and Definitions UD UN USP 9696 unit declaration UN USP given UT1 UTn importing unit declaration UN UE 9696 unit definition A 3 5 Unit Expressions UE UT unit term AUNI1 SP1 UNn SPn e UT unit composition A 3 6 Unit Terms UT UT with SM 9696 symbol translation UT hide SL 96596 hiding listed symbols UT reveal SM 9696 revealing translating symbols UTI and and UTn 9696 amalgamation local UD1 UDn within UT local units UN 9696 unit name UN UT1 fit SM1 UTn fit SMn functional unit application Page 102 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 A 4 Libraries 103 A A Libraries library LN named library of downloadings specifications views A 4 1 Downloadings from LN get IN1 INn end downloads listed items from LN get IN gt IN end renames downloaded items A 4 2 Library Names LN BASIC NUMBERS 9696 greatest version installed BASIC
5. spec NAT free type Nat 0 suc pre Nat preds lt gt _ lt _ gt Nat x Nat even odd Nat ops Nat Nat os min _ __ Nat x Nat Nat 1 _ div_ Nat x Nat Nat Operations to represent natural numbers with digits ops 1 Nat suc 0 1_def_Nat 2 Nat suc 1 2_def_Nat 3 Nat suc 2 3_def_Nat 4 Nat suc 3 96 4 def Nat 96 5 Nat suc 4 5 def_Nat 6 Nat suc 5 6_def_Nat 7 Nat suc 6 7_def_Nat 8 Nat suc 7 8_def_Nat 9 Nat suc 8 9_def_Nat Page 107 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 108 B Basic Library QQ m Nat n Nat Nat m suc 9 n decimal_def sort Pos p Nat e p gt 0 ops 1 Pos suc 0 1_as_Pos_def Pos x Pos Pos 2 2 Pos x Nat Pos Nat x Pos Pos suc Nat Pos end spec INT NAT then generated type Int Nat Nat sort Nat lt Int 9696 a system of representatives for sort Int is 9696 a 0 and 0 p where a Nat and p Pos preds lt gt lt gt Int x Int even odd Int Ops _ sign Int Int abs Int Nat min Int x Int Int Int x Nat Int __ _ div_ quot_ rem Int x Int Int _ mod__ Int x Int Nat end spec RAT INT then generated type Rat __ __ Int Pos sort Int lt Rat preds lt lt gt gt Rat x Rat ops
6. Page 49 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 50 6 Structuring Specifications Elem x Stack Stack not only the operation name is changed but also its profile according to the renaming of List into Stack In a symbol map one can qualify the symbol to be renamed by its kind using the keywords sort op and pred or their plural forms as appropriate this is illustrated in STACK above Qualification in symbol maps is generally recommended since it improves their readability While it is possible to change the syntax of an operation or predicate symbol as illustrated above for cons mapped to push__onto__ it is not possible to change the order of the arguments of the renamed operation or predicate In general one does not need to rename all the symbols provided by the specification to be renamed In the symbol map describing the intended re naming it is indeed enough to mention only the symbols that change By default any symbol not explicitly mentioned is left unchanged although its profile may be updated according to the renaming specified for some sorts This is illustrated here in STACK where there is no need to rename the constant empty which will therefore have the same name for both lists and stacks How ever the induced signature morphism maps the constant symbol empty List into the constant symbol empty Stack One can also explicitly rename a symbol to itself say by writing empty empty or ju
7. _ abs Rat Rat LL min max Rat x Rat Rat Rat x Rat Rat Rat x Int Rat end B 2 Library Basic StructuredDatatypes This library provides specifications which formalize structuring concepts of data as used e g for the design of algorithms or within programming lan guages Its main focus are advanced concepts as e g finite sets lists strings Page 108 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 B 2 Library Basic StructuredDatatypes 109 finite maps finite bags arrays and various kinds of trees But is also cov ers some elementary constructions like the encapsulation of data within a maybe type or arranging data as pairs Common to all these concepts is that they are generic Consequently all specifications of this library are pa rameterized Finite sets finite maps and finite bags are specified in terms of observers given a generated sort an operation or predicate is introduced in order to define equality on this sort Concerning finite sets equality on the sort FinSet Elem is characterized using the predicate eps displayed as in the specification GENERATEFINSET Finite maps i e elements of the sort FinMap S T are considered to be identical if their evaluation under the operation eval yields the same result c f the specification GENERATEFIN In the specification GENERATEBAG those elements of sort Bag Elem are identified that show the same frequen
8. and with Elem gt Nat When convenient the instantiation can be completed by a renaming as illustrated in the following variant of spec NAT WORD 1 GENERIC Monor NXTURAL with Monoid Nat Word end Page 59 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 60 7 Generic Specifications Fitting of operations and predications can sometimes be left implicit too and can imply fitting of sorts spec LIST_ORDER_NAT List Oper ORDER end In the above example the fitting of both symbols of the parameter of the sort Elem the binary predicate __ lt __ can be left implicit in the instantiation because the argument NATURAL ORDER has only single symbols of the right kind The coincidence of the predicate symbol in the parameter and argument is irrelevant here Fitting of function and predicate symbols can imply fitting of sorts For in stance when a parameter predicate symbol is fitted to an argument predicate symbol whose profile involves different sorts this implies that the parameter sorts involved have to be fitted to the corresponding sorts in the argument specification Note also that in the above example checking the definedness of the in stantiation corresponds to a non trivial proof obligation The instantiation is defined since the predicate lt provided by NATURAL ORDER is indeed a total ordering relation hence the properties required by are fulf
9. components ELEM Similarly we name the specification ELEM gt ELEM Then both named spec ifications can be reused in the architectural specification which is essentially the same as the architectural ein Generic specifications naturally give rise to specifications of generic com ponents which can be named for later reuse as illustrated above by CoNT However the reader should not confuse a generic specification which is nothing else than a piece of specification that can easily be adapted by in stantiation with the corresponding specification of a generic component the Page 208 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 8 2 Explicit Generic Components 209 latter cannot be instantiated it is the specified generic component which gets applied to suitable components Persistent extensions of the form spec SP2 SP1 then SP also natu rally give rise to specifications of generic components of the form SP1 SP2 as illustrated by DEL In the architectural specification we use again the fact that the generic component F can be applied to richer arguments than models of and similarly for G Since ELEM more general has more mod els than NATURAL there are potentially fewer possibilities for implementing the generic component specified by Cont_Comp which should be compat ible with any model of ELEM than there are for implementing the generic component specified
10. pre z y e x pre y suc z y 0 e r suc y 2 e r pre y 2 7 Tn specification libraries ordinary decimal notation for natural numbers be provided by use of so called literal syntax annotations see Chap 9 20 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 3 Free Specifications 21 While a case distinction with respect to the constructors of a free datatype is harmless this may not be the case for a datatype defined within a freeness constraint since due to the axioms relating the constructors to each other some cases may overlap This does not mean however that one cannot use the case distinction but just that more attention should be paid than for a free datatype For instance in the above example no problem arises But one should be more careful with the next one since a negative integer can be of the form suc x hence asserting e g 0 lt suc x would of course be wrong spec INTEGER_ARITHMETIC_ORDER then preds lt lt gt lt gt i Int x Int y Int 0x0 0 lt pre 0 0 0 lt 0 0 lt pre z suc zx y amp x lt pre y pre z lt y amp x suc y 2 gt 9 lt 2 lt 2 lt gt lt Generic specifications often involve free extensions of loose ters spec LIST sort Elem free type List empty
11. A 1 2 Variables and Axioms var 0 8 global variable declaration vars vl 51 un sn global variables declaration vars Ul Un Sn abbreviated variables declaration multiple global variable declarations Vu s e Fn universal quantification on axiom lists Vul 81 vn sn universal quantifications on axiom lists V Ul un sn 9696 abbreviated quantifications Moss idis oos 9696 multiple quantifications on axiom lists e Fn unquantified axiom lists A 1 2 1 Formulae V eF 99 universal quantification on formula d e F existential quantification qd e F unique existential quantification Fi Fn 9696 conjunction FIV V Fn 9696 disjunction implication F if F reverse implication Fer 9696 equivalence F negation true truth false 90 falsity p T1 Tn predicate application tO T1 t1 Tn tn mixfix predicate application q constant predicate T T ordinary strong equality T T existential equality TEs subsort membership A 1 2 2 Terms T f T1 application 10 t1 Tn tn mixfix application 10 T1 Tn t1 literal syntax constant T s 9696 sorted term ass 9696 projection to subsort T when F else T conditional choice Page 98 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 A 1 Basic Specifications 99 A 1 3 Symbols Characte
12. Page 16 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 2 Generated Specifications 17 Note also that this example displays the power of the annotation implies which is used here not only to stress that the usual properties of insert are expected to follow from the preceding declarations and axioms but also that an alternative induction scheme based on empty __ and U _ can be used for sets Moreover it asserts that 0 16 expected to be associative commutative idempotent i e US S and to have empty for unit Note again that this implies part heavily relies on the same name same meaning principle Generated types may need to be declared together The following specification fragment illustrates what may go wrong sort Node generated type Tree mktree Node Forest generated type Forest empty add Tree Forest The above is both incorrect due to the linear visibility rule and wrong since the corresponding semantics is not what a naive reader may expect One may expect that only the minimal fixpoint interpretation of the above mutually recursive definitions of the datatypes Tree and Forest is acceptable but indeed any fixpoint interpretation is which means that for instance a model with both a junk tree obtained from a node and a junk forest by mktree and a junk forest obtained from a junk tree and an empty forest by add fulfills the above declarations Hence one must write inste
13. SN result F CN SN The architectural specification is a variant of CONT2SET NAT where instead of requiring a component N implementing NATURAL and two generic components implementing containers and sets re spectively we just require a component CN implementing containers of nat ural numbers and a component SN implementing sets of natural numbers However then the application F CN SN makes no sense since there is no way to ensure that the common symbols of CN and SN have the same inter pretation It may indeed be the case that natural numbers are interpreted in some way in CN and in a different way in N which makes the application of F impossible Let us now consider a more complex example arch spec BADLY STRUCTURED ARCH SPEC units N A C 3 result F C A N S N The architectural specification BADLY STRUCTURED ARCH SPEC is a vari ant of ue d where in addition to the component N imple menting we require a generic component A which is used to expand N into an implementation of In the architectural specification the compatibility condition in the ap plication F S N was easy to discharge Here in the result unit term F C AUNT S A N of STRUCTURED Ancir Seec we apply F to the pair made of C A N and 5 A N In this case only a semantic analysis can ensure that these two arguments are compatible since the com mon symbols cannot be trac
14. cons Elem List end The parameter of a generic specification should be loose to cope with the various expected instantiations On the other hand it is a frequent situation that the body of the generic specification should have a free initial interpre tation This is illustrated by the above example where we want to combine a loose interpretation for the sort Elem with a free interpretation for lists The following example is similar in spirit spec SET sort Elem free type Set empty insert Elem Set pred _is_in__ Elem x Set Ve e Elem S Set e insert e insert e insert e S e insert e insert e insert e insert e S Page 21 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 22 3 Total Many Sorted Specifications e is_in empty e e is in insert e S e is in insert e S if e is in S end As for the LisT example we want to have a loose interpretation for the sort Elem and a free interpretation for sets Since some axioms are required to hold for the Set constructors empty and insert we cannot use a free datatype declaration hence we use a freeness constraint Note that since as already explained predicates hold minimally in models of free specifications it would have been enough in the above example to define the predicate is by the sole axiom e is in insert e S However doing so would have decreased the comprehensibility of the specification and this is the reason
15. end spec GENERATEK TREE k Int ek gt 1 Cond_nonEmptyBranching sort Elem given INT ARRAY ops 1 Int k Int fit ops min Int 1 Int gt sort K Tree k Elem fit sort Elem Elem then free type KTree k Elem nil kTree entry Elem branches Array Tree k Elem end spec KTREE op Int ek gt 1 Cond_nonEmptyBranching sort Elem given INT GENERATEK TREE op k Int sort Elem and FINSET sort Elem then def preds isEmpty isLeaf K Tree k Elem isCompound Tree K Tree k Elem Elem x K Tree k Elem ops height KTree k Elem Nat maxHeight Index x Array K Tree k Elem Nat leaves KTree k Elem FinSet Elem allLeaves Index x Array KTree k Elem FinSet Elem end spec GENERATEN TREE sort Elem List sort N Tree Elem fit sort Elem gt N Tree Elem then free type NTree Elem nil n Tree entry Elem branches List N Tree Elem end Page 113 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 114 B Basic Library spec NTREE sort Elem given NAT GENERATENTREE sort Elem and FINSET sort Elem then preds isEmpty isLeaf NTree Elem isCompound Tree NTree Elem Elem x N Tree Elem ops height NTree Elem Nat maxHeight List NTree Elem Nat leaves NTree Elem FinSet Elem allLeaves List NTree Elem FinSet Elem end Page 114 FIRST PUBL
16. spec PUMP_CONTROLLER_FAILURE SBCS_STATE_4 then pred Pump_Controller_OK State x FinSet R Message x PumpNumber Vs State msgs FinSet R_Message pn PumpNumber e Pump Controller OK s msgs pn lt PCS predicted s pn Unknown PCS V PCS predicted s pn SoonFlow v PUMP_CONTROLLER_STATE pn PCS predicted s pn as PumpControllerState msgs end C 5 5 Detection of the Steam and Water Level Measurement Device Failures To specify the failures of the steam and water level measurement devices we must again rely on some predicted values Here however we cannot predict an exact value but only an interval in which the received value should be contained This leads to the following extension of spec SBCS STATE 5 SBCS STATE 4 then free type Valpair pair low Value high Value ops steam predicted level predicted State Valpair 4 low steam_predicted s is the minimal output of steam predicted high steam_predicted s is the maximal output of steam predicted and similarly for level predicted Y 96 end The specification of the failures of the measurement devices is again straightforward and is given in the and specifications Remember that the meaning of Steam OK Level OK resp is only relevant when Transmission holds which in particular implies that there is only one STEAM v LEVEL v resp message in msgs hence only one possible v in the quantifications Vv Value below Note also that
17. 32 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 4 3 Partial Selectors and Constructors 33 spec LIST_SELECTORS_2 sort Elem sort Elem then ops head List Elem tail List List Ve Elem L List def head empty def tail empty head cons e L e tail cons e L L end The above specification is an alternative to both specifications define exactly the same class of models However is clearly easier to understand and can be con sidered as technically simpler since it involves no freeness constraint Operations like head and tail are usually called selectors and CASL pro vides abbreviations to specify selectors in a very concise way as we see next 4 3 Partial Selectors and Constructors Selectors can be specified concisely in datatype declarations and are usually partial spec Lisr SELECTORS sort Elem free type List empty cons head Elem tail List end The above free datatype declaration introduces in addition to the con structors empty and cons two partial selectors head and tail yielding the respective arguments of the constructor cons Hence this free datatype decla ration with selectors has exactly the same effect as the ordinary free datatype declaration free type List empty cons Elem List together with the operation declarations and axioms of i e SELECTORS and LisT SELECTORS 2 define exactly the same class of models The following exam
18. caused by the then and and keywords in the specifications while the double arrows denote hiding caused by the local then parts in the specifica tions By klicking on the nodes one can inspect their signatures In this way we can see that both LIST ORDER SORTED and LIST_ORDER have the same signature Hence it is legal to write a view view v2 TOTAL ORDER lLisT ORDER SORTED TOTAL ORDER to LIST TOTAL_ORDER By again typing end hets g Sorting casl we now get the following development graph shown in Fig 10 3 Internal nodes in a development graph correspond to unnamed parts of a structured specification In comparison with Fig 10 2 there are now two new internal nodes corresponding to the instantiations of both Lis ORDER SORTED and ORDER with TOTAL ORDER For each of the instantiations a proof obligation is generated which here is a dashed arrow from TOTAL ORDER to itself since TOTAL ORDER is simultaneously the formal and the actual parameter Page 78 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 1 The Heterogeneous Tool Set Hets 79 Total_Order List_Selectors List_Order_Sorted Fig 10 2 Development graph for the two sorting specifications Proof obligations can be discharged in various ways A trivial proof obligation as the above one can be discharged by Hets alone using the 277 menu The interesting proof obligation in Fig 10 3 is the lower menu s
19. empty as ax iom implies that choose S is defined for any S since the term empty is always defined To understand this assume that choose is undefined for some set value of S then the above equation cannot hold for this value since the undefinedness of choose S implies the undefinedness of remove choose S insert choose S empty giving a contradiction with the definedness of empty Hence an equation between a term involving a partial function PF and a term involving total functions only may imply that the partial function PF is always defined e Asserting insert choose S 5 S as an axiom implies that choose S is defined for any S since a variable always denotes a defined value This case is indeed similar to the previous one the only difference being that now the right hand side of the equation is a variable instead of a term involving total functions only Moreover the same name same thing principle has a subtle side effect re garding partial operations if an operation is declared both as a total operation and as a partial operation with the same profile i e the same argument sorts and the same result sort then it is interpreted as a total operation in all models of the specification 4 2 Specifying Domains of Definition The definedness of a term can be checked or asserted Page 29 FIRST PUBLIC DRAFT 17 S8ep 2003 17 54 30 4 Partial Functions spec SET_PARTIAL CHOOSE_1 sort Elem
20. then op elements_of _ Cont Elem Set Ve Elem Cont Elem e elements_of empty empty e clements of insert e e U elements_of C end arch spec ARCH CONT2SET NAT result F C N S N The architectural specification ARCH CONT2SET NAT requires a compo nent N implementing N ATURAL a generic component C implementing CONT i e containers and a generic component 5 implementing SET COMP i e sets Then it further requires a generic component F that given any pair of compatible models X of tal erben bd maren ELEM expands them into a model of ELEM Models X and Y are said to be compatible if they share a common interpre tation for all symbols they have in common Here the only symbol they have in common is the sort Elem so the compatibility condition means that X and Y have the same carrier set for Elem Compatibility is a natural condition since it is obviously necessary that X and Y have a common interpretation of their common symbols otherwise they cannot be both expandable to the same more complex component The compatibility condition is a bit more subtle in the presence of subsorts for more details see Mos03 Secs 1 3 1 2 III 5 1 Page 211 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 212 8 Specifying Architectural Structure The result is then obtained by applying F to the pair obtained by applying C to and S to N Here the pair of arguments C N and S N
21. ALGEBRA version 0 999 specified version installed HTTP greatest version uninstalled HTTP version 1 0 2 specified version uninstalled Page 103 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 B Basic Library Markus Roggenbach Till Mossakowski and Lutz Schroder The Cast Basic Library consist of specifications of often needed datatypes and view among them freeing the specifier from re inventing well know things This can be compared to standard libraries in programming languages While this user manual often discusses several styles of specifying with CASL the basic datatypes consistently follow a certain style described in VI 12 We here describe two of the libraries cf the overview in Fig B 1 the library of numbers and of structured datatypes We also provide stripped down versions of the libraries themselves with some of the specification and all axioms and annotations removed This stripped down version can serve for getting a first overview over the signatures of the specified datatypes The full Cast Basic Library is printed in the CASL Reference Manual VI The latest version is available at http www tzi de cofi The Hets tool described in Chap allows you to obtain a graphical overview over the specifications in the libraries and also inspect their signa tures We recommend to do this in order to get a better overview and also for answering specific questions that arise when using the basic
22. ARCH CONT2SET USED we can then describe a closed system made of a component N implementing and of an open system CSF specified by which is then applied to N in the result part Page 212 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 3 Writing Meaningful Architectural Specifications 213 8 3 Writing Meaningful Architectural Specifications In the previous sections we have already pointed out potential sources of in consistent specifications of components Another issue which deserves some attention when designing an architectural specification is compatibility be tween components or more generally unit terms that are to be combined together either by and or by fitting them to a generic component with mul tiple arguments In an architectural specification it is advisable to ensure that any shared symbol between two components or unit terms that are to be combined can be traced to a single non generic component arch spec ARCH_CONT2SET_NAT_V result N The architectural specification is a variant of where instead of declaring a generic component F with two arguments we now declare a generic component G with a single argument which must be a model of the specification Cont ELEM and ELEM obtained as the union of the two trivially in stantiated specifications of containers and sets As a consequence to obtain the desired system in the result part we apply the generic com
23. Boiler Control Specification Problem For completeness the text describing the case study description as originally provided by Jean Raymond Abrial is reproduced here C 12 1 Introduction This text constitutes an informal specification of a program which serves to control the level of water in a steam boiler It is important that the program works correctly because the quantity of water present when the steam boiler is working has to be neither too low nor to high otherwise the steam boiler or the turbine sitting in front of it might be seriously affected Page 148 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 12 The Steam Boiler Control Specification Problem 149 The proposed specification is derived fom an original text that has been written by LtCol J C Bauer for the Institute for Risk Research of the Uni versity of Waterloo Ontario Canada The original text has been submitted as a competition problem to be solved by the participants to the International Software Safety Symposium organized by the Institute for Risk Research It has been given to us by the Institut de Protection et de Stret Nucl aire Fontenay aux Roses France We would like to thank the author the Institute for Risk Research and the Institut de Protection et de S ret Nucl aire for their kind permission to use their text The text to follow is severely biased to a particular implementation This is very often the case with industrial specifications that
24. Each unit declaration listed in an architectural specification corre sponds to a separate implementation task independent from the other ones For instance in the architectural specification the task of provid ing a component D expanding C and implementing NATURAL Page 204 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 1 Architectural Specifications 205 is independent from the tasks of providing implementations N of and C of NATURAL Hence when providing the component D one cannot make any further assumption on how the component C is or will be implemented besides what is expressly ensured by its specification To understand this let us consider again the requirements specification or its variant FLAT Among its models there is one where con tainers are implemented by lists without repetitions and in this model we can choose to implement delete by just removing the first found occurrence of the element to be deleted In this model however we rely on the knowledge about the implementation of containers to decide how to implement delete which is fine since both are simultaneously implemented in the same model In con trast in the architectural specification we request that containers are to be implemented in the component C while delete is to be provided by a separate component D Imposing that the component D can be devel oped independently of the component C means that for D it is no longer possible t
25. List Elem x Elem Nat end Page 110 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 B 2 Library Basic StructuredDatatypes 111 spec GENERATEFINMAP sort 5 sort T mono generated type FinMap S T empty FinMap S T T S op eval 5 x FinMap S T end spec FINMAP sort 5 sort T given NAT mono GENERATEFINMAP sort 5 sort and FINSET sort 5 fit Elem gt gt 5 and FINSET sort T fit Elem T then def free type Entry S T target T source S preds isEmpty FinMap S T 6 Entry S T x FinMap S T Lus gt FinMap S T x FinSet S x FinSet T Ops FinMap S T x Entry S T FinMap S T FinMap S T x S FinMap S T FinMap S T x T FinMap S T dom FinMap S T FinSet S range FinMap S T FinSet T U FinMap S T x FinMap S T FinMap S T end spec GENERATEBAG sort Elem given NAT mono generated type 3 Bag Elem Elem freq Bag Elem x Elem Nat end spec Bac sort Elem given NAT mono GENERATEBAG sort Elem then preds isEmpty Bag Elem Elem x Bag Elem _C__ Bag Elem x Bag Elem ops Elem x Bag Elem Bag Elem Bag Elem x Elem Bag Elem U N Bag Elem x Bag Elem Bag Elem end spec ARRAY ops min maz Int e min lt Cond_nonEmptyIndex sort Elem Page 111 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 112 B Basi
26. MONOID sort Elem sort Elem then When the parameter and the argument have symbols in common these parameter symbols are implicitly taken to fit directly to the corresponding ar gument symbols Thus it is never necessary to make explicit that a symbol is mapped identically In the above example for instance the parameter specifi cation of GENERIC MONOID 18 exactly the same as the argument specification in its instantiation so the fitting can be left implicit The fitting of parameter sorts to unique argument sorts can also be left implicit spec NAT WORD Generic Mosoib NATURAL end Page 58 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 7 1 Parameters and Instantiation 59 When the argument specification has only a single sort the fitting of all parameter sorts to that sort is obvious and can again be left implicit Of course this does not apply the other way round if the parameter has a single sort which is often the case in practice but the argument specification has more than one sort the parameter sort could be mapped to any of the argu ment sorts so the fitting symbol map has to be made explicit except when the parameter sort is identical to one of the argument sorts as previously explained Fitting symbol maps determine fitting morphisms A fitting signature morphism from the signature of the parameter part to the signature of the argument specification is automat
27. Maximal normal Outcome of steam at the exit of the steam boiler W litre sec quantity U litre sec sec Maximum gradient of increase Us litre sec sec Maximum gradient of decrease Capacity of each pump litre sec Nominal capacity Current measures q litre Quantity of water in the steam boiler p litre sec Throughput of the pumps U litre sec Quantity of steam exiting the steam boiler C 12 3 The overall operation of the program The program communicates with the physical units through messages which are transmitted over a number of dedicated lines connecting each physical unit with the control unit In first approximation the time for transmission can be neglected The program follows a cycle and a priori does not terminate This cycle takes place each five seconds and consists of the following actions Page 151 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 152 C Case Study The Steam Boiler Control System e Reception of messages coming from the physical units e Analysis of informations which have been received e Transmission of messages to the physical units To simplify matters and in first approximation all messages coming from or going to the physical units are supposed to be received emitted simultane ously by the program at each cycle C 12 4 Operation modes of the program The program operates in different modes namely initializati
28. PhysicalUnit FAILURE ACKNOWLEDGEMENT PhysicalUnit junk end For the received messages in addition to the messages specified in Sec 12 6 we add an extra constant message junk This message will represent any re ceived message which does not belong to the class of recognized messages We do not add a similar message to the messages sent since we may assume that the steam boiler control system will only send proper messages Obviously receiving a junk message will lead to the detection of a failure of the message transmission system In the SBcs Csr specification we describe the various constants that char acterize the Steam Boiler see Sec C 12 2 Page 119 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 120 C Case Study The Steam Boiler Control System spec SBcs_CsT then ops C M1 M2 N1 N2 W U1 U2 P Value dt Value 9696 Time duration between two cycles 5 sec These constants must verify some obvious properties e 0 lt M1 e M1 lt N1 N1 lt N2 e N2 lt M2e 2 lt e 0 lt W e 0 lt UL e 0 lt U2 e OK lt P end We will also specify the datatypes set of received messages and set of sent messages since as suggested at the end of Sec 1213 all messages supposed to be received or emitted simultaneously at each cycle The two latter specifications are obtained by instantiation of a generic specification FINSET of sets of elements This generic specificatio
29. Pump pn else Flow when PUMP CONTROLLER STATE pn Flow msgs V PUMP_CONTROLLER_STATE pn NoFlow msgs PCS predicted s pn SoonFlow pn chosen pumps s msgs Closed else NoFlow when pn chosen pumps s msgs Closed PUMP CONTROLLER STATE pn NoFlow msgs PCS predicted s pn SoonFlow pn chosen pumps s msgs Open else SoonFlow end All our predictions are summarized in the following spec ification spec PU_PREDICTION and 4 Both specifications extend instantiated by FAILURE DETECTION and 1 end Page 140 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 C 7 Specifying the Messages to Send 141 C 7 Specifying the Messages to Send At this stage we are left with the specification of the messages to send at each cycle This is easily specified following Sec 5 and leads to the following specification The specification is obtained by instantiating the EVOLUTION specification by and extending the result by the specification of the operation messages to send spec SBCS ANALYSIS then local ops PumpMessages FailureDetectionMessages State x FinSet R Message gt FinSet S Message Repaired AcknowledgementMessages FinSet R Message gt FinSet S Message Vs State msgs FinSet R Message Smsg S Message e Smsg PumpMessages s msgs gt Jpn PumpNumber e pn chosen_pumps s msgs Open Smsg O
30. R Message Mode 121 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 122 C Case Study The Steam Boiler Control System spec STEAM_BOILER_CONTROL_SYSTEM SBCS_ANALYSIS then op init State pred is_step State x FinSet R Message x FinSet S Message x State Specification of the initial state init by means of the observers e g e mode init Normal e Specification of is step by means of the observers and of the updating operations e g 96 Vs s State msgs FinSet R Message Smsg FinSet S Message e is step s msgs Smsg s lt gt mode s next mode s msgs A Smsg messages to send s msgs then 9696 Specification of the reachable states free pred reach State Vs s State msgs FinSet R Message Smsg FinSet S Message e reach init e reach s is_step s msgs Smsg s gt reach s end Of course the specification SBCS ANALYSIS is likely to be further struc tured into smaller pieces of specifications Indeed since the informal require ments are too complex to be handled as a whole we will therefore succes sively concentrate on various parts of them The study and formalization of each chunk of requirements will lead to specifications that will later on be put together to obtain the SBCS_ANALYSIS specification As already pointed out it is likely that when analyzing a chunk of requirements we will discover the need for new observers on states i e new state variables Th
31. are allowed Subsorts are interpreted as embeddings Axioms are first order formulae built from definedness assertions and both strong and existential equations Sort generation constraints can be stated Datatype declarations are provided for concise specification of sorts equipped with some constructors and optional selectors including enumerations and products Structured specifications Allow translation reduction union and extension of specifications Extensions may be required to be conservative and or free initiality con straints are a special case A simple form of generic parameterized specifications is provided to gether with instantiation involving parameter fitting translations Architectural specifications Express that the specified software is to be composed from separately developed reusable units with clear interfaces Libraries Allow the distributed storage and retrieval of particular versions of named specifications 96 A CASL Quick Reference A 1 Basic Specifications sorts op preds types 5 in any order but declaration before use sort declarations and definitions wes 9696 operation declarations and definitions 9696 predicate declarations and definitions 9696 datatype declarations and definitions generated 9696 sort generation constraint vars V e Fn 9696 global variable declarations 9696 universal quantification on lists of ax
32. are rarely indepen dent from a certain implementation people have in mind In that sense this specification is realistic Your first formal specification steps could be much more abstract if that seems important to you in particular if your formalism allows you to do so In other words you are encouraged to structure your specification in a way that is not necessarily the same as the one proposed in what follows But in any case you are asked to demonstrate that your specification can be refined to an implementation that is close enough to the functional requirements of the specification proposed below You might also judge that the specification contain some loose ends and inconsistencies Do not hesitate to point them out and to take yourself some appropriate decisions The idea however is that such inconsistencies should be solely within the organization of the system and not within its physical properties We are aware of the fact that the text to follow does not propose any precise model of the physical evolution of the system only elementary suggestions As a consequence you may have to take some simple even simplistic abstract decisions concerning such a physical model C 12 2 Physical environment The system comprises the following units the steam boiler a device to measure the quantity of water in the steam boiler four pumps to provide the steam boiler with water four devices to supervise the pumps one controller f
33. by NATURAL which only needs to be compatible with models of a similar argument holds for Cour As a consequence the variant is not equivalent to the architectural specification So far we have always used named structured specifications to specify components Un named specifications can be used as well as illustrated below unit spec DEL CoMP1 ELEM op dolere Elem x Cont Elem Cont Elem Ve e Elem e e is in dela sl QC e e isin C e DEL DEL_ComP1 DEL_Comp is a variant of DEL COMP where for the sake of the exam ple we directly specify the delete operation instead of referring to the named specification CONT DEL Remember that in a specification of a generic com ponent of the form SP1 SP2 SP2 is always considered as an implicit extension of SP1 which explains why the above example is well formed A generic component may be applied more than once in the same architectural specification result F N and F C fit Elem RGB The above architectural specification requires a component N specified by a component C specified by and a generic component F specified by CONT COMP Then as described by the result part the de sired system is obtained by applying F to N applying F to C in this case an explicit fitting symbol map is necessary since COLOUR exports two sorts Page 209 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 210 8 Specif
34. can exist since NATURAL is a persistent extension of Consider now the following variant of and the associated vari ant of the architectural specification Page 205 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 206 8 Specifying Architectural Structure spec CoNT DEL V ELEM then op delete Elem x Cont Elem Cont Elem Ve Elem Cont Elem e delete e empty empty e delete e insert e C C when e else insert e delete e C e e is in delete e e isin C e e end arch spec INCONSISTENT units NATURAL CoNT NXrURAL given N given result D The specification NATURAL is consistent has some mod els but is not a persistent extension of NATURAL since for instance a model of NATURAL where containers are realized by arbitrary lists possibly with repetitions cannot be expanded into a model of NATURAL As a consequence in the architectural specie RoR the specification of the component D is inconsistent since no compo nent can expand all implementations C of NATURAL into models of NATURAL The architectural specification is therefore itself inconsistent To summarize architectural specifications not only prescribe the intended architecture of the implementation of the system but they also ensure that the specified components can be developed independently of each other which
35. den Brand P E Moreau and J J Vinju Environments for term rewriting engines for free In R Nieuwenhuis editor Proceedings of the 14th International Conference on Rewriting Techniques and Applica tions RTA 03 volume 2706 of LNCS pages 424 435 Springer Verlag 2003 M G J van den Brand J Scheerder J J Vinju and E Visser Dis ambiguation filters for Scannerless Generalized LR parsers In R Nigel Horspool editor Compiler Construction volume 2304 of LNCS pages 143 158 Springer Verlag 2002 CoFI The Common Framework Initiative for algebraic specification and development electronic archives Notes and Documents accessible from Feng Chen Grigore Rosu and Ram Prasad Venkatesan Rule based anal ysis of dimensional safety In R Nieuwenhuis editor Proceedings of the 14th International Conference on Rewriting Techniques and Applications RTA 03 volume 2706 of LNCS pages 197 207 Springer Verlag 2003 158 References DHK96 GB92 KR00 Mos00 Mos02 Mos03 Pau94 Page 158 A van Deursen J Heering and P Klint editors Language Prototyp ing An Algebraic Specification Approach volume 5 of AMAST Series in Computing World Scientific 1996 Joseph A Goguen and Rodney M Burstall Institutions abstract model theory for specification and programming Journal of the ACM 39 1 95 146 1992 H l ne Kirchner and Christophe Ringeissen Executing CASL equational specifications with the ELAN r
36. dt x high adjusted steam s msgs Page 138 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 6 Predicting the Behaviour of the Steam Boiler 139 e high next level predicted s msgs min C high adjusted level s msgs maximal pumped water s msgs dt x U2 2 dt x low adjusted steam s msgs e Dangerous WaterLevel s msgs lt gt low next level predicted s msgs lt M1 V lt high next level predicted s msgs hide ops minimal pumped water maximal_pumped_water end C 6 2 Predicting the Pump and Pump Controller States Specifying the predicted state of each pump at the next cycle is almost trivial The next pump state is Unknown PS if the nezt_status of the pump is not OK otherwise it should be Open if e itis Open now and the pump is not ordered to stop or e the pump is ordered to activate otherwise it should be Closed since e itis Closed now and the pump is not ordered to activate or e itis ordered to stop This leads to the following specification This specification extends since we rely on chosen pumps for our predictions and which provides next status instantiated by which provides the pred icate PU OK parameter of spec PUMP STATE PREDICTION Faune DETECTION and then nezt_PS_predicted State x FinSet R Message x PumpNumber ExtendedPumpState Vs State msgs FinSet R Message pn PumpNumber e next PS predicted s msgs pn Unknown P
37. e g applied twice to the same set argument they return the same result Datatypes with observer operations can be specified as generated in stead of free spec SET GENERATED sort Elem generated type Set empty insert Elem Set pred _is_in__ Elem x Set Ve Elem 8 5 Set e e is in empty e e is in insert e S amp e V e is in 8 e S S Elem e x is in S lt is_in S end The above specification is an alternative to the specification given on p Both and define exactly the same class of models The former specification relies on a freeness constraint while GENERATED relies on the observer is in to specify when two sets are equal For the purpose of this example we disregard the fact that choose should be un defined on the empty set and we just leave this case unspecified Partial functions are discussed in Chap Page 23 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 24 3 Total Many Sorted Specifications Indeed the last axiom of SET GENERATED expresses directly that two sets having exactly the same elements are equal values This axiom together with the first two axioms defining is in will entail as well the expected properties on the constructor insert see on p 16 Note also that since inSET GENERATED the predicate is 2n is not defined within a freeness constraint we specify when it holds using rather than 1 way implication While a freeness
38. e weight cons e L weight e weight L end In the above example we specialize lists of arbitrary elements to lists of elements equipped with a weight operation which is then overloaded by a weight operation on lists Therefore we specify that the generic specification has for parameter a specification extending the given E E EUN a sort Elem and an operation sym bol weight Thereby the intention is to emphasize the fact that only the sort Elem and the operation weight are intended to be specialized when the spec ification will be instantiated and not the fixed part One could have written also spec LisT WEIGHTED ELEM NATURAL ARITHMETIC then sort Elem op weight Elem Nat but the latter which is correct misses the essential distinction between the part which is intended to be specialized and the part which is fixed since by definition the parameter is the part which has to be specialized Note also that omitting the given NATURAL clause would make the declaration spec Lisr WEIGHTED ELEM sort Elem op weight Elem Nat ill formed since the sort Nat is not available To summarize the given construct is useful to distinguish the true pa rameter from the part which is fixed Both the parameter and the body of the generic specification extend what is provided by the given part whose exported symbols are therefore available Page 66 FIRST PUBLIC DR
39. failure of the message transmission system e g the stop order was not properly sent or was not received or the message indicating the pump state has been corrupted or a failure of the pump which was not able to execute the stop order or which sends incorrect state messages Our understanding of the requirements is that in such a case we must conclude there has been a failure of the pump not of the message transmission system Let us stress again that it is important to distinguish between the actual failures of the various pieces of equipment and the diagnosis we will make Only the latter is relevant in our specification C 5 1 Understanding the Detection of Equipment Failures Before starting to specify the detection of equipment failures we must proceed to a careful analysis of Sec 1217 in order to clarify the inter dependencies mentioned above Only then will we be able to understand how to structure our specification of this crucial part of the problem Page 126 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 C 5 Specifying the Detection of Equipment Failures 127 A first rough analysis of the part of Sec C 12 7 devoted to the description of potential failures of the physical units i e of the pumps the pump con trollers and the two measuring devices shows that these failures are detected on the basis of the information contained in the received messages we must check that the received values are in accordance with so
40. free datatype construct with selectors hence have a free interpretation SET_PARTIAL_CHOOSE_2 is itself an extension of PARTIAL_CHOOSE which is an extension of GENERATED SET where sets are defined by a generated datatype construct However note that as discussed in Chap p the apparently loose specification GENERATED SET is in fact not so Moreover the choose partial function on sets is loosely defined in SET_ and so is therefore also the choose partial function on Page 48 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 6 2 Renaming 49 lists defined in List_CHOOSE It is easy to see that the operation elements_of is uniquely defined The sort Elem has of course a loose interpretation Thus the specification _ combines parts with a free interpre tation parts with a generated interpretation and parts with a loose interpre tation The situation is similar to that with and SET_TO_LIST where the operation list_of is loosely defined with the help of the operation elements 6 2 Renaming Renaming may be used to avoid unintended name clashes or to adjust names of sorts and change notations for operations and predicates spec STACK sort Elem sort Elem with sort List Stack ops cons push onto head top tail pop end While the same name same thing principle has proven to be appropri ate in numerous examples given in the previous ch
41. from reuse of specifications from existing libraries The rest of this chapter illustrates the constructs used to specify local libraries distributed libraries and versions and gives some advice on the organization of libraries 9 1 Local Libraries Local libraries are self contained collections of specifications library USERMANUAL EXAMPLES spec NATURAL spec NATURAL_ORDER NATURAL then Page 218 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 9 1 Local Libraries 219 The collection of all the illustrative examples given in the foregoing chap ters is self contained so it could be made into a local library and named USERMANUAL EXAMPLES as outlined above It would also be possible to divide our illustrative examples into local libraries according to a general classification of datatypes ordering relations numbers lists sets etc with a further library for miscellaneous datatypes such as that of vehicles This or ganization would facilitate browsing the illustrative specifications concerned with particular kinds of datatypes However some duplication of specifica tions would be required e g natural numbers are needed in connection with both lists and vehicles The same name same thing principle of CASL applies only within specifi cations and it is possible for a library to include alternative specifications for the same symbols e g using different sets of axioms However when such alternat
42. have seen already when either the vital units have a failure or when the water level risks to reach one of its two limit values This mode can also be reached after detection of an erroneous transmission between the program and the physical units This mode can also be set directly from outside Once the program has reached the Emergency stop mode the physical environment is then responsible to take appropriate actions and the program stops Page 153 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 154 C Case Study The Steam Boiler Control System C 12 5 Messages sent by the program The following messages can be sent by the program e MODE m The program sends at each cycle its current mode of opera tion to the physical units e PROGRAM READY In initialization mode as soon as the program as sumes to be ready this message is continuously sent until the message PHYSICAL UNITS READY coming from the physical units has been re ceived e VALVE In initialization mode this message is sent to the physical units to request opening and then closure of the valve for evacuation of water from the steam boiler OPEN PUMP n This message is sent to the physical units to activate a pump e CLOSE PUMP n This message is sent to the physical units to stop a pump e PUMP FAILURE DETECTION n This message is sent until receipt of the corresponding acknowledgement to indicate to the physical units that the program has detected a pump f
43. imposes a certain degree of genericity for these components 8 2 Explicit Generic Components Genericity of components can be made explicit in architectural speci fications G result G The architectural specification is a variant of here we choose to specify the second and third components as explicit generic components Page 206 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 8 2 Explicit Generic Components 207 The line P Navona Coxa declares a generic component Given any component implementing i e model of F should expand it into an implementation of that the result model expands the argument model The third component G is also specified as a generic component given any implementation of NATURAL should expand it into an imple mentation of CONT_DEL NATURAL Hence the whole system is obtained by the composition of applications as described in the result part In CASL such compositions are called unit terms The component of corresponds to the application F N in and similarly the component D in SYSTEM corresponds to G C i e to G F N in SvsrEM G A specification of the form SP1 SP2 defines generic components GC that should always expand their argument into a model of the target speci fication This makes only sense as long as the signature of the target speci fication contains the signature of SP1 This is why in CASL SP2 is alwa
44. in order to avoid the tedious repetition of the declaration of the variables and y for each list of axioms we have used here global variable declaration which introduces x and y for the rest of the specification Variable declarations are of course not exported across specification extensions the variables and y declared VARIANT OF TOTAL ORDER WITH MINMAX are not visible in any of its extensions Symbols may be conveniently displayed as usual mathematical symbols by means of display annotations Adisplay 1eq LATEX _ lt __ spec PARTIAL ORDER then pred z y Elem x y V x y end The above example relies on a 96display annotation while for obvious reasons the specification text should be input using the ISO Latin 1 char acter set it is often convenient to display some symbols differently e g as mathematical symbols This is the case here where the leq predicate symbol is more conveniently displayed as lt Display annotations as any other CASL annotations are auxiliary parts of a specification for use by tools and do not affect the semantics of the specification In the above example we have again used the facility of simultaneously declaring and defining a symbol here the predicate symbol lt in order to obtain a more concise specification The 96implies annotation is used to indicate that some axioms are supposed to be consequences of others s
45. indicated above the library BAsiC STRUCTUREDDATATYPES does not itself provide the specifications of natural numbers and integers that are needed in the specifications of LIST and ARRAY but instead downloads Nat and INT from the BASIC NUMBERS library The names of the items to be downloaded from a library have to be listed explicitly one cannot request the downloading of all the items that happen to be provided by a library However although the name of each item provided by a downloading is always explicit no indication is given of its kind 1 whether it is an ordinary generic or architectural specification or a view nor of what symbols it declares Thus the well formedness of a library depends on what items are actually downloaded from other libraries The item from get above has the effect of downloading the spec ifications that are named NAT and INT in BASIC NUMBERS preserving their names It is also possible to give downloaded specifications different names e g to avoid clashes with names that are already in use locally from Basic NUMBERS get NAT gt NATURAL INT gt INTEGER Page 224 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 9 2 Distributed Libraries 225 Items that are referenced by downloaded items are not themselves auto matically downloaded e g downloading INT does not entail the downloading of NAT This is because downloading involves the semantics of the named items not their text The sem
46. insert Page 22 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 3 Free Specifications 23 Nat without fixing its value yet this value is likely to be fixed later in some refinements and all that we need for now is the existence of some bound This is provided by the above specification where we mix an initial interpretation for the sort Nat defined using a free datatype declaration in NATURAL and a loose interpretation for the constant maz size Each model of will provide a fixed interpretation of the constant maz size and all these models are captured by NATURAL_WITH_ which is in this sense loose Using such loose extensions is in general appropriate to avoid unnecessary overspecification spec SET_CHOOSE sort Elem sort Elem then op choose Set Elem VS Set e 5 empty gt choose S is in S end This example shows again the benefit of mixing initial and loose seman tics Here we want to extend sets defined using a free constraint in by a loosely specified operation choose At this stage the only property required for choose is to provide some element belonging to the set to which it is ap plied and we do not want to specify more precisely which specific element is to be chosen Note that each model of SET CHOOSE will provide a function implementing some specific choice strategy and that since all these interpreta tions of choose have to be functions they are necessarily deterministic
47. is abstracted here in a predicate addable so far left unspecified Later on instantiations of the PART CONTAINER specification can be adapted to specific purposes by extending them with axioms defining addable The above generated datatype declaration abbreviates as usual the dec laration of a sort P Container a constant constructor empty and a partial constructor insert Elem x P Container P Container It also entails the corresponding generatedness constraint Page 34 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 4 4 Existential equality 35 4 4 Existential equality Existential equality involves the definedness of both terms as well as their equality spec NATURAL_PARTIAL_SUBTRACTION_2 NATURAL_PARTIAL_SUBTRACTION_1 then Vz y Nat y x z 4r gt y 2 z would be wrong 2 2 gt 2 is correct but better abbreviated the above axiom end An existential equation t1 t2 is equivalent to def t1 def t2 11 t2 so it holds if and only if both terms 1 and t2 are defined and denote the same value Note that while a trivial strong equation of the form t t always holds this is not the case for existential equations For instance the trivial existential equation y y does not hold since the term y may be undefined In general consequences of undefinedness are undesirable Hence a con ditional equation o
48. lt Steam OK s msgs e PU OK s msgs WaterLevel lt Level OK s msgs hide ops Pump_OK Pump Controller Steam_OK Level OK end C 6 Predicting the Behaviour of the Steam Boiler In the previous section we have explained that failure detection was to a large extent based on a comparison between the received messages and the expected Page 134 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 6 Predicting the Behaviour of the Steam Boiler 135 ones For this purpose we have extended the specification by several observers which means we have assumed that each cycle we record in some state variables the information needed to compute the expected messages at the next cycle According to our explanations in Sec we must now specify for each observer obs introduced a corresponding next_obs operation This is the aim of this section We have already defined the operation nezt_mode in the generic specifica tion see C 4 and the operation nezt_status in the generic specification see Sec 5 2 Thus what is left is the specification of the operations PS predicted next PCS predicted next steam predicted and next level predicted As explained in C 5 the informal requirements suggest that we should take into account some inter dependencies when predicting values to be re ceived at the next cycle For instance the water level in the steam boiler depends on how much steam is produced but also on how
49. message three times in a row The aim of the predicate SystemStillControllable is to characterize the conditions under which the steam boiler control system will operate in Rescue mode Let us point out that the corresponding part of the infor mal requirements see Sec 12 4 4 is not totally clear in particular the exact meaning of the sentence if one can rely upon the information which comes from the units for controlling the pumps There is a double am biguity here on the one hand it is unclear whether the pumps means all pumps or at least one pump on the other hand there are two ways of controlling each pump the information sent by the pump and the information sent by the pump controller and it is unclear whether controlling refers to both of them or only to the pump controller Our interpretation will be as follows we consider it is enough that at least one pump is correctly working and for us correctly working will mean we rely on both the pump and the associated pump controller As with all interpretations made during the formalization process we should in principle interact with the designers of the informal requirements in order to clarify what was the exact intended meaning and to check that our interpretation is adequate The important point is that our interpreta tion is entirely localized in the axiomatization of SystemStillControllable and it will therefore be fairly easy to change
50. message which has been emitted previously by the program STEAM FAILURE ACKNOWLEDGEMENT By this message the phys ical units acknowledge the receipt of the corresponding failure detection message which has been emitted previously by the program C 12 7 Detection of equipment failures The following erroneous kinds of behaviour are distinguished to decide whether certain physical units have a failure PUMP 1 Assume that the program has sent a start or stop message to a pump The program detects that during the following transmission that pump does not indicate its having effectively been started or stopped 2 The program detects that the pump changes its state spontaneously PUMP CONTROLLER 1 Assume that the program has sent a start or stop message to a pump The program detects that during the second transmission after the start or stop message the pump does not indicate that the water is flowing or is not flowing this despite of the fact that the program knows from elsewhere that the pump is working correctly 2 The program detects that the unit changes its state spontaneously WATER_LEVEL_MEASURING_UNIT 1 The program detects that the unit indicates a value which is out of the valid static limits that is between 0 and C 2 The program detects that the unit indicates a value which is incompatible with the dynamics of the system STEAM LEVEL MEASURING UNIT 1 The program detects that the unit indicates a value which is out o
51. normal forms or may not terminate ELAN can be called either as interpreter or as complier Here is an example of how the ELAN interpreter is called gt fenv2elan GT pred fenv sort bool interp To Efix To REF warning the query sort is bool index 428 ELAN version 3 4 03 12 99 19 39 c LORIA CNRS INPL INRIA UHP U Nancy 2 1994 1999 Import form file GT pred Importing Identifiers Importing Sorts Importing Modules Importing RuleNames Importing StrategyNames enter query term finished by the key word end s s zero gt s zero end start with term Page 83 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 84 10 Tools s s zero gt s zero result term true end enter query term finished by the key word end s zero gt s s zero end start with term s zero gt s s zero result term false end Here is an example of how the ELAN compiler is called gt fenv2elan GT_pred fenv sort bool compil 11 Efix To REF warning the query sort is bool index 428 Reduce ELAN Machine v 2 1 c LORIA CNRS INPL INRIA UHP U Nancy 2 1998 1999 2000 Author P E Moreau Reduce ELAN Machine Reading from file GT pred ref Parsing The compiled query is not ground Compiling nonamed rules Compiling strategies execute the following line to build you
52. of steam has been repaired Page 154 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 12 The Steam Boiler Control Specification Problem 155 C 12 6 Messages received by the program The following messages can be received by the program STOP When the message has been received three times in a row by the program the program must go into emergency stop STEAM_BOILER_WAITING When this message is received in initializa tion mode it triggers the effective start of the program PHYSICAL UNITS READY This message when received in initialization mode acknowledges the message PROGRAM READY which has been sent previously by the program PUMP STATE n b This message indicates the state of pump n open or closed This message must be present during each transmission PUMP_CONTROL_STATE n b This message gives the information which comes from the control unit of pump n there is flow of water or there is no flow of water This message must be present during each transmission LEVEL v This message contains the information which comes from the water level measuring unit This message must be present during each transmission STEAM v This message contains the information which comes from the unit which measures the outcome of steam This message must be present during each transmission PUMP REPAIRED n This message indicates that the corresponding pump has been repaired It is sent by the physical units until a corre sponding acknow
53. only the pumps which are re liable and already Open will pour some water in the broken pumps the pumps which are just ordered to activate and the pumps which are or dered to stop are all considered not pouring water in Similarly to compute maximal pumped water we consider that the pumps which are reliable and already Open the pumps which are just ordered to activate as well as all the broken pumps may pour some water in only the reliable pumps Page 136 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 6 Predicting the Behaviour of the Steam Boiler 137 just ordered to stop or already stopped are known not to be pouring any water in 7 Finally we can predict the interval in which the water level is expected to stay during the next cycle For this we use two auxiliary operations low_predicted_level and high_predicted_level to compute the lower and upper bounds of this interval 8 This prediction is the basis for deciding whether the water level risks to reach a Dangerous WaterLevel 1 below M1 or above M2 Note that the intervals in which the output of steam and the water level are expected to stay during the next cycle are predicted without considering the neri status of these devices This is indeed necessary for the Degraded and Rescue operating modes This leads to the following STEAM AND LEVEL PREDICTION specification spec STEAM AND LEVEL PREDICTION FAILURE DETECTION sort PumpNumber
54. our practical experience this step is usually very fruitful from an engineering point of view and one could argue that the benefits to be expected here are enough in themselves to justify the use of formal methods even if for lack of time or other resources no full formal development of the system is performed b Once we have a sufficient understanding of the problem to be specified we must translate the informal requirements into a formal specifica tion This step will require us to provide interpretations for the unclear or missing parts of the informal requirements Moreover this formal ization process will also be helpful to further detect inconsistencies and loose ends in the informal requirements Here a very important issue is to keep track of the interpretations made during the formaliza tion process in order to be able later on to take into account further modifications and changes of the informal requirements c When we have written the formal requirements specification we must carefully check its adequacy with respect to the informal requirements this part is called the validation of the formal specification In principle there should be some interaction between the specification team and the team who has designed the informal requirements in par ticular to check whether the suggested interpretations of the detected loose ends are adequate In the framework of this case study however such in teractions were not possi
55. pair low Value high Value then Basics fit S PhysicalUnit sort Status and Basics fit S PumpNumber sort ExtendedPumpState and Basics fit S PumpNumber sort ExtendedPumpControllerState then free type ConcreteState state mode Mode nbSTOP Nat status_map TotalFinMap PhysicalUnit Status PS predicted TotalFinMap PumpNumber ExtendedPumpState PCS predicted TotalFinMap PumpNumber ExtendedPumpControllerState steam predicted level predicted Valpair ops s atus s ConcreteState pu PhysicalUnit Status eval pu status map s PS predicted s ConcreteState pn PumpNumber ExtendedPumpState eval pn PS predicted map s PCS predicted s ConcreteState pn PumpNumber ExtendedPump ControllerState eval pn PCS predicted end Page 146 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 10 Designing the Architecture of the Steam Boiler Control System 147 The specification SBCS STATE Spcs_ANALYSIS of the component A of ARCH SBCS be refined into the following architectural specification arch spec ARCH_ANALYSIS units FD Sucs_Srare EALURE DETEHON PR Eucuns Dereerros s PU ME Nee En FU MTS ANALYSIS result AS SBCS STATE IPR FD end In the above architectural specification the component FD provides an implementation of failure detection t
56. so some more words should be added here otherwise Hets has to be removed here 82 10 Tools e choosing a shallow embedding of CASL into HOL e g CASL s logical im plication gt is mapped directly to Isabelle HOL s logical implication gt and the same holds for other logical connectives and quantifiers and e adapting Isabelle HOL s syntax to be conform with the CASL syntax e g Isabelle HOL s gt is displayed as gt as in CASL However it is essential to be aware of the fact that the Isabelle HOL logic is different from the CASL logic Therefore the formulas appearing in subgoals of proofs with HOL CASL will not fully conform to the CASL syntax they may use features of Isabelle HOL such as higher order functions that are not present in CASL and moreover they also may contain syntax from the meta logic Pure e g meta implication gt meta universal quantification and meta variables x HOL CAsL can be obtained under http www tzi de cofi To start the HOL CASL system follow the installation instructions and then type HOL CASL You can load the above specification file Order casl by typing use casl Order Lets try to prove part of the view above To prepare proving in the target specification of the view NATURAL ORDER 1I type in CASL context Natural Order II casl AddsimpAllO The first command just selects the specification as current proving context the second one adds all the
57. sort then def choose empty VS Set def choose S gt 8 is in S end definedness assertion written def t where t is a term is a special kind of atomic formula it holds if and only if the value of the term is defined For instance in the above example def choose empty explicitly asserts that choose is undefined when applied to empty Note that this axiom does not say anything about the definedness of choose applied to values other than empty which means that choose may well be undefined on those values too The second axiom of the above example asserts choose S is in 5 under the condition def choose S to avoid undesired definedness induced by axioms as explained above Note that if the two axioms of the above example were to be replaced by VS Set e S empty gt choose S is in S then we could conclude that choose S is defined when 5 is not equal to empty but nothing about the undefinedness of choose empty The domains of definition of partial functions can be specified exactly spec SET PARTIAL CHOOSE 2 sort Elem Se0 PARTIAL CHOOSE sort Elem then VS Set e def choose S 5 empty VS Set def choose S 8 is in S end In the above example the domain of definition of the partial function choose is exactly specified by the axiom def choose S lt gt 5 empty Loosely specified domains of definition may be useful spec N
58. specification Instead one should impose a freeness constraint around the datatype declaration followed by the required axioms A freeness constraint expressed by the keyword free can be imposed around any spec ification In the case of the above INTEGER specification the freeness constraint im poses that the semantics of the specification is the quotient of the constructor terms by the minimal congruence induced by the given axioms and hence provides exactly the desired semantics More generally a freeness constraint around a specification indicates its initial model which may of course not exist It is however well known that initial models of basic specifications with axioms restricted to Horn clauses always exist Remember also that equality holds minimally in initial models of equational specifications Predicates hold minimally in models of free specifications spec NATURAL_ORDER then free pred _ lt _ Nat x Nat Nat e 0 lt e lt gt lt suc y A freeness constraint imposed around a predicate declaration followed by some defining axioms has the effect that the predicate only holds when this follows from the given axioms and does not hold otherwise For instance in the above example it is not necessary to explicitly state that 0 lt 0 since this will follow from the imposed freeness constraint Hence in such cases a freeness constraint has exact
59. state that choose S Elem when S is not the empty set moreover to make the term choose S is in S well formed we have to explicitly overload the predicate is in Elem x Set provided by GENERATED SET by a predicate is in ElemError x Set as shown above This example demonstrates that avoiding partial functions by the use of error supersorts is not as innocuous as it may seem since in general one would need to enlarge the signatures considerably by adding all required overloadings spec SET_ERROR_CHOOSE_1 sort Elem sort Elem then sorts Elem lt ElemError op choose Set ElemError VS Set e 5 empty choose S as Elem is in S end The specification SET ERROR CHOOSE 1 above is a last attempt to avoid the use of partial functions again we introduce a supersort ElemError as in SET ERROR CHOOSE but to avoid the need for overloading the predicate is in we explicitly cast the term choose S in choose S as Elem is_in S Note that when for some value of 5 choose S as Elem is in S holds this implies that choose S as Elem is defined and hence that choose S Elem holds as well This last version may seem preferable to the previous one However one should be aware that here despite our attempt to avoid the use of partial functions we rely on explicit casts hence on terms that may not denote values partiality has not been eliminated the partial functions have merely been factorized as compo
60. the changes in the new versions and adapting the downloading library accord ingly For instance one might download INT from the current version of BA SIC NUMBERS instead of from version 1 0 of that library This may involve extra work when a new version of BASIC NUMBERS appears but it has sev eral advantages over the more cautious approach CASL leaves the choice to the user although registered libraries will generally be required to use explicit version numbers when downloading from other libraries Page 227 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 228 9 Libraries By the way the current version of a library is not necessarily the one most recently installed it is the one with the largest version number As previously mentioned a patched version 0 99 1 could be installed after version 1 0 but a downloading without an explicit version number would still refer to version 1 0 Previous versions of libraries are to remain accessible for ever at least in principle In practice however older versions of libraries can be made inac cessible after checking that no accessible versions of other libraries download anything from them Page 228 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 Tools Till Mossakowski 10 1 The Heterogeneous Tool Set Hets The Heterogeneous Tool Set Hets is the central analysis tool for CASL Hets is a tool set for the analysis and encoding of specifications written in
61. then local ops received steam State x FinSet R Message Value adjusted steam State x FinSet R Message Valpair low predicted steam high predicted steam State x FinSet R Message Value received level State x FinSet R Message Value adjusted level State x FinSet R Message Valpair low predicted level high predicted level State x FinSet R Message Value broken pumps Statex FinSet R_Message gt FinSet PumpNumber reliable_pumps State x FinSet R Message PumpState gt FinSet PumpNumber Vs State msgs FinSet R Message pn PumpNumber ps PumpState 9696 Axioms for STEAM e Transmission s msgs gt STEAM received steam s msgs msgs e adjusted steam s msgs pair received steam s msgs received steam s msgs when Transmission s msgs PU OK s msgs OutputOfSteam else steam predicted s 9696 Axioms for LEVEL e Transmission s msgs gt LEVEL received level s msgs msgs e adjusted level s msgs pair received level s msgs received level s msgs when Transmission OK s msgs PU OK s msgs WaterLevel else level predicted s 9696 Axioms for auxiliary pumps operations Page 137 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 138 C Case Study The Steam Boiler Control System e pn broken_pumps s msgs gt PU_OK s msgs Pump pn PU OK s msgs PumpController pn e pn reliable_pumps s m
62. x Nat y Nat e 0 lt e lt 0 e suc r lt suc y amp z y end view v1 STRICT PARTIAL ORDER to NATURAL ORDER Elem Nat end Again these specifications can be checked with Hets However this check ing does only encompass syntactic and static semantic well formedness it is not checked whether the naturals actually are a strict partial order Checking this requires theorem proving which will be covered later Hets also displays and manages proof obligations using development graphs However even without theorem proving it is interesting to inspect the proof obligations arising from a specification This can be done with hets g Order casl Hets now displays a so called development graph which is just an overview graph showing the overall structure of the specifications in the library see Fig Page 76 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 1 The Heterogeneous Tool Set Hets EC Strict_Partial_Order Natural Order Il Fig 10 1 Sample development graph Nodes in a development graph correspond to CASL specifications Ar rows show how basic specification are linked through the structuring constructs The solid arrow denotes an ordinary import of specifications caused by the then while the dashed arrow denotes a proof obligation caused by the view This proof obligation needs to be discharged in order to show that the view is well f
63. 003 17 54 C 9 Validation of the CASL Requirements Specification 143 Specification of is_step Vs s State msgs FinSet R_Message Smsg FinSet S Message e is slep s msgs Smsg s gt mode s next_mode s msgs nbSTOP s next nbSTOP s msgs PhysicalUnit e status s pu next status s msgs pu Vpn PumpNumber e PS predicted s pn next PS predicted s msgs pn PCS predicted s pn next PCS predicted s msgs pn steam predicted s next steam predicted s msgs level predicted s next level predicted s msgs Smsg messages to send s msgs then Specification of the reachable states free pred reach State Vs s State msgs FinSet R Message Smsg FinSet S Message e reach init e reach s is step s msgs Smsg s gt reach s end C 9 Validation of the CASL Requirements Specification Once the formalization of the informal requirements is completed we must now face the following question is our formal specification adequate Answer ing this question is a difficult issue since there is no formal way to establish the adequacy of a formal specification w r t informal requirements i e we cannot prove this adequacy However we can try to test it by performing various experiments When these experiments are successful we increase our confidence in the formal specification If some experiment fails then we can inspect the specificati
64. 03 17 54 Copyright to be clarified with Springer and Abrial Important Note The Additional Information that was also provided is not reproduced here see LNCS 1165 page 507 148 C Case Study The Steam Boiler Control System Finally we refine the specification FAILURE DETECTION gt of the component PR of the architectural specification ARCH ANALYSIS as fol lows arch spec ARCH PREDICTION units SE FAILURE DETECTION TATUS EVOLUTION FAILURE DETECTION FAILURE DETECTION gt STEAM AND LEVEL PREDICTION EVOLUTION FAILURE_DETECTION X STEAM AND LEVEL PREDICTION MP STATE PREDICTION SLP PP PCP PUMP_CONTROLLER_STATE_PREDICTION result FD FAILURE DETECTION e loca D D SLPFD SLP FD within SEFD SLPFD and PCP SEFD SLPFD l end In the above architectural specification the component SE provides an im plementation of next status The component SLP provides an implementation of next steam predicted next level predicted chosen pumps and Dangerous WaterLevel The component PP provides an implementation of next PS predicted and the component provides an implementation of PCS predicted We are now left with specifications of components that are simple enough to be directly implemented and this concludes our case study C 11 Conclusion Some concluding words will eventually be added here C 12 The Steam
65. 17 54 A 2 Structured Specifications 101 2 Structured Specifications A 2 1 Specifications SP SP with SM symbol translation SP hide SL 9696 hiding listed symbols SP reveal SM revealing translating symbols SP1 and and SPn union SP1 then then SPn extension free SP free or initial local SP within SP implicit hiding of local symbols closed SP 9696 non extension SN reference to named specification SN FA1 FAn instantiation of generic specification A 2 2 Named and Generic Specifications spec SN SP end named specification end optional spec SN SP1 SPn SP generic specification spec SN SP1 SPn 9696 generic with imports given SP1 SPm SP A 2 2 1 Fitting Arguments FA SP fit SM fitting by symbol map SP implicit fitting FV fitting view A 2 3 Named and Parametrized Views view VN SP to SP named view end optional SM end view VNISP1 SPn 9696 generic view SP to SP SM view VNISP1 SPn generic view with imports given SP1 SPm SP to SP SM A 2 3 1 Fitting Views FV view VN reference to named view view VN FA1 FAn 9696 instantiation of generic view Page 101 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 102 A CASL Quick Reference A 2 4 Symbol Lists SZ and Maps SM SY1 5Yn lists maybe with sorts ops preds SY1 e SY1 SYn SYn maps maybe with sorts ops preds
66. 2 We leave VALUE as an implicit parameter of our specifications rather than us ing generic specifications taking VALUE as a parameter since our specifications are not to be instantiated by argument specifications describing several kinds of values but on the contrary should all refer to the same abstract datatype of values It is of course possible to take measuring units into account following for in stance the method described in CRV03 Appropriate CASL libraries supporting measuring units are currently being developed 118 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 C 2 Getting Started 119 spec BASICS free type PumpNumber Pump1 Pump2 Pump3 2 free type PumpState Open Closed free type PumpControllerState Flow NoFlow free type PhysicalUnit Pump PumpNumber PumpController PumpNumber OutputOfSteam WaterLevel free type Mode Initialization Normal Degraded iud Rescue EmergencyStop spec MESSAGES SENT then free type S Message MODE Mode PROGRAM READY VALVE OPEN PUMP PumpNumber CLOSE PUMP PumpNumber FAILURE DETECTION PhysicalUnit REPAIRED ACKNOWLEDGEMENT PhysicalUnit end spec MESSAGES RECEIVED Basics and then free type R_Message STOP STEAM BOILER WAITING PHYSICAL UNITS READY PUMP STATE PumpNumber PumpState PUMP CONTROLLER STATE PumpNumber PumpControllerState LEVEL Value STEAM Value REPAIRED
67. AFT 17 Sep 2003 17 54 7 3 Parameters with Fixed Parts 67 Argument specifications are always implicitly regarded as extension of the imports spec LIST_WEIGHTED_PAIR_NATURAL_COLOUR LisT_WEIGHTED_ELEM PAIR NATURAL_COLOUR fit Elem Pair weight gt first end The instantiation specified in List WEIGHTED_PAIR NATURAL_COLOUR is correct since the fitting map is the identity on all the symbols exported by the fixed part which happens here to be included in the argument specification PAIR NATURAL_COLOUR More generally the argument specification is always regarded as an extension of the given fixed part and the fitting map should be the identity on all symbols this fixed part exports This is illustrated in the next example spec LIST_WEIGHTED_INSTANTIATED sort Value op weight Value Nat Here we rely on a rather trivial instantiation whose purpose is merely to illustrate our point where the fitting symbol map can be omitted since no ambiguity arises and where the argument specification sort Value op weight Value Nat is well formed because it is regarded as an extension of the given NATURAL ARITHMETIO fixed part of 5 WEIGHTED ELEM which implies the sort Nat is available end Imports are also useful to prevent ill formed instantiations spec LisT LENGTH sort Elem given NATURAL ARITHMETIC sort Elem then op length List El
68. ATURAL WITH BOUND AND ADDITION then op _ __ Nat x Nat Nat y Nat e def x y if z 4 y lt maz_size 96 x y lt maz size implies both x lt maz size and y lt maz_size 96 e def a y gt a y at y end Page 30 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 4 2 Specifying Domains of Definition 31 In some cases it is useful to loosely specify the domain of definition of a partial function as illustrated in the above example for which is required to be defined for all arguments and y such that x y lt maz_size but may well be defined on larger natural numbers as well The point in loose specifications of definition domains is to avoid unnecessary constraints on the models of the specification For instance the above example does not exclude a model where is interpreted by a total function which would then coincide with Indeed in some cases specifying exactly domains of definition can be con sidered as overspecification In most specifications however one would expect an exact specification of domains of definition even for otherwise loosely spec ified functions see e g choose SET _PARTIAL_CHOOSE_2 Domains of definition can be specified more or less explicitly spec SET PARTIAL CHOOSE 3 sort Elem sort Elem then def choose empty VS Set S empty gt choose S is in S end SET PARTIAL CHOOSE 3 specifies exa
69. C The Common Framework Initiative for algebraic specification and development Michel Bidoit and Peter D Mosses User Manual FIRST PUBLIC DRAFT September 17 2003 Springer Berlin Heidelberg New York Hong Kong London Milan Paris Tokyo Preface CASL the Common Algebraic Specification Language has been designed by the Common Framework Initiative for algebraic specification and de velopment It is an expressive language for specifying requirements and design for conventional software It is algebraic in the sense that models of CASL specifications are algebras the axioms can be arbitrary first order formulae From CASL simpler languages e g with axioms restricted to conditional equations for interfacing with existing tools are obtained by restriction and CASL is also extended in more advanced languages e g higher order CASL strikes a happy balance between simplicity and expressiveness This User Manual illustrates and discusses how to write CASL speci fications Content This CASL User Manual introduces the potential user to the features of CASL mainly by means of illustrative examples It presents and discusses the typical ways in which the language concepts and constructs are expected to be used in the course of building system specifications Thus the presentation focuses on what the constructs and concepts of CASL are for and how they should and should not be used W
70. CASL HOL CASL is an interactive theorem prover for CASL based on the tactic prover Isabelle The HOL CASL system provides an interface between CASL and the theorem proving system Isabelle HOL Pau94 We have chosen Isabelle because it has a very small core guaranteeing correctness and its provers like the simplifier or the tableaux prover are built on top of this core Furthermore there is over ten years of experience with it several mathematical textbooks have partially been verified with Isabelle Isabelle is a tactic based theorem prover implemented in standard ML The main Isabelle logic called Pure is some weak intuitionistic type theory with polymorphism The logic Pure is used to represent a variety of logics within Isabelle one of them being HOL higher order logic For example logical implication in Pure written gt also called meta implication is different from logical implication in HOL written gt also called object implication CASL now is in turn represented in Isabelle HOL Since subsorting and partiality are present in CASL but not in Isabelle HOL we have to encode them out follwoing the lines of Mos02 This means that theorem proving is not done in the CASL logic directly but in the logic HOL for higher order logic of Isabelle HOL CAsL tries to make user s life easy by Page 81 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 Hets will provide this in the future hopefully in September if
71. CASL its extensions and sublanguages hence the name heterogeneous The latest version can be obtained under epp eterne eri The in stallation is easy just follow the instructions Consider the first example in this User Manual spec STRICT PARTIAL ORDER Let s start with a simple example sort Elem pred lt Elem x Elem pred abbreviates predicate 2 Elem e z lt x strict e lt lt asymmetric lt lt 2 gt 2 lt 2 transitive 7 4 Note that there may exist x y such that neither x lt y nor y lt x end 1 Hets also is available on the CD coming with the CASL reference manual 76 10 Tools Hets can be used for checking static well formedness of specifications Let us assume that the example is written to a file named Order casl actually this file is provided on the web and on the CD Then you can check the well formedness of the specification by typing in hets Order casl Hets both checks the correctness with respect to the CASL syntax as well as the static semantics correctness e g whether all identifiers have been declared before they are used whether the sorting is correct whether the use of overloaded symbols is unambiguous and so on Now the natural numbers form a strict partial order which can be ex pressed by a view as follows spec NATURAL free type Nat 0 suc Nat end spec NATURAL ORDER then pred _ lt Nat
72. IC DRAFT 17 Sep 2003 17 54 Case Study Steam Boiler Control System In this chapter we illustrate the use of CASL on a fairly large and complex case study the Steam boiler control system We describe how to derive a CASL specification of the steam boiler control system starting from the informal re quirements provided to the participants of the Dagstuhl Meeting Methods for Semantics and Specification organized jointly by Jean Raymond Abrial Egon Borger and Hans Langmaack in June 1995 1 The aim of this formalization process is to analyze the informal requirements to detect inconsistencies and loose ends and to translate the requirements into a formal algebraic CASL specification During this process we have to provide interpretations for the unclear or missing parts We explain how we can keep track of these additional interpretations by localizing very precisely in the formal specification where they lead to specific axioms thereby taking care of the traceability issues We also explain how the CASL specification is obtained in a stepwise way by successive analysis of various parts of the problem description Emphasis is put on how to specify the detection of the steam boiler failures Finally we discuss validation of the CASL requirements specification resulting from the formalization process and in a last step we refine the requirements specifica tion in a sequence of architectural specifications that describe the i
73. In MORE_VEHICLE we introduce a further subsort Boat of Vehicle and as a consequence we again get the effect of having both maz_speed and weight available for boats as it was already the case for cars and bikes Subsort membership can be checked or asserted spec SPEED_REGULATION then ops speed limit Vehicle Nat car speed limit bike speed limit Nat Vv Vehicle e v Car speed limit v car speed limit e v Bicycle gt speed limit v bike speed limit end subsort membership assertion written t s where t is a term and s is a sort is a special kind of atomic formula it holds if and only if the value of the term is the embedding of some value of sort s For instance in the above example v Car holds if and only if v denotes a vehicle which is the embedding of a car value Note that is input as in but displayed as Datatype declarations can involve subsort declarations The specification sorts Car Bicycle Boat type Vehicle sort Car sort Bicycle sort Boat is equivalent to the declaration sorts Car Bicycle Boat lt Vehicle There may be some values of sort Vehicle which are not the embedding of any value of sort Car Bicycle or Boat Intuitively the above datatype declaration just means that Vehicle contains the union which may not be disjoint of Car Bicycle and Boat Note that the subsorts used in the datatype declaration m
74. LAT REQ have the same models which illustrates our point about the fact that the CASL specification building operations are merely facilities to structure the text of specifications into coherent units An architectural specification consists of a list of unit declarations specifying the required components followed by a result part indicating how these components are to be combined arch spec SYSTEM units C N given D NATURAL given C result D The SysTEM architectural specification is intended to prescribe a specific architecture for implementing the system specified by REQ The first part introduced by the keyword units indicates that we require the implementation of our system to be made of three components and D The second part introduced by the keyword result indicates that the component D provides the desired implementation Each component is provided with its specification The line N declares a component N specified by NATURAL which means simply that should be a model of Page 203 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 204 8 Specifying Architectural Structure The line Cont NATURAL given N declares a component C which given the previously declared component N provides a model of NATURAL It is essential to understand that the component C must expand the assumed component N into a model of NATURAL which means that C reduced to the si
75. L_PARTIAL_SUBTRACTION N N N N N N N N N N Page 166 FIRST PUBLIC DRAFT NATURAL_PARTIAL_SUBTRACTION_1 82 NATURAL_PARTIAL_SUBTRACTION_2 NATURAL_PARTIAL_SUBTRACTION_3 51 NATURAL_PARTIAL_SUBTRACTION_4 NATURAL_POSITIVE_ARITHMETIC NATURAL_SUBSORTS NATURAL_SUC_PRE NATURAL_WITH_BOUND NATURAL_WITH_BOUND_AND _ ADDITION NON_GENERIC_MONOID TREE UMBERS ZZ OTHER SvsTEM 209 OTHER_SYSTEM_1 PAIR 109 PAIR 1 PAIR NATURAL COLOUR PAIR NATURAL COLOUR 1 PAIR NATURAL COLOUR 2 PArR Pos Pos 1 PART CONTAINER PARTIAL ORDER 9 PARTIAL_ORDER_1 19 PARTIAL ORDER 2 POSITIVE POSITIVE_ARITHMETIC POSITIVE_PRE PRELIMINARY 120 PU_PREDICTION PUMP_CONTROLLER_FAILURE 133 PuMP_CONTROLLER_STATE_ PREDICTION 1140 PUMP_FAILURE 132 PuMP STATE PREDICTION Ram 107 108 REQ 203 SBCS ANALYSIS 141 SBcs Csr 120 SBCs STATE 142 17 Sep 2003 17 54 SBCS STATE 1 SBCS STATE 2 SBCS STATE 3 SBCS_STATE_4 132 SBCS_STATE_5 1133 SBCS STATE IMPL SET SET AND LisT SET CHOOSE SET CoMwP 211 SET ERROR CHOOSE SET ERROR CHOOSE 1 SET_GENERATED SET_OF_LIST SET_PARTIAL_CHOOSE SET_PARTIAL_CHOOSE_1 SET PARTIAL CHOOSE 2 SET PARTIAL CHOOSE 3 SET_TO_LIST SET_UNION SetT_UNION_1 SPEED_REGULATION STACK STATUS_EVOLUTION STEAM_AND_LEVEL_PREDICTION STEAM_BOILER_CONTROL_SYSTEM 142 Page 167 FIRST PUBLIC DRAFT 129 Index of Library and Sp
76. MW 202 202 202 Pie aii dak ak Bye aid 203 cm 203 SYSTEM ied err ebrei dea paa e pad qr er 203 DUET 204 eT Xx ane een ae 206 206 EI 206 207 T 208 vu 208 Im 208 TTE TU ECTETUR T 209 up 209 T 210 T 211 Page 161 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 162 Named Specifications be oie stints Spee San a ee c te 211 211 212 212 Wine DAS ea ee O 213 Der 214 pnr 214 UC PTT 215 215 Em 16 TL 76 a bade dla Pika ba ek 78 PPP 105 pL 105 RP 106 RATE ET r rm 107 STRUCTUREDDATATYPES esses 108 EP 109 r m 109 En 109 TIL 109 fM NTC EH MERE E 109 CH 109 vH 109 rm 109 ies es eee M 109 TT 118 TI RR eae ae heb 119 119 UEM AME 119 Nive yard ote dae te eh 120 Si aye hens teed nae sant Au
77. PEN PUMP pn pn chosen_pumps s msgs Closed Smsg CLOSE PUMP pn e Smsg FailureDetectionMessages s msgs PhysicalUnit e Smsg FAILURE DETECTION pu status s msgs pu FailureWithoutAck e Smsg RepairedAcknowledgementMessages msgs lt gt PhysicalUnit e Smsg REPAIRED ACKNOWLEDGEMENT pu nezt_status s msgs pu FailureWithAck es cS within messages_to_send Statex FinSet R Message FinSet S Message Vs State msgs FinSet R_Message e messages_to_send s msgs PumpMessages s msgs U FailureDetectionMessages s msgs U RepairedAcknowledgementMessages msgs MODE next mode s msgs end Page 141 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Perhaps a better alternative is to choose arbitrary values and not bother the reader with this initialization phase 142 C Case Study The Steam Boiler Control System C 8 The Steam Boiler Control System Specification According to our work plan detailed in Sec we have already specified the main parts of our case study First let us display a basic flat specifica tion equivalent to 5 8 STATE 5 where all the state observers are listed together spec SBCS_STATE then sort State free type Status Failure WithoutAck Failure WithAck free type ExtendedPumpState sort PumpState Unknown PS free type ExtendedPumpControllerState sort Pump Contr
78. S when next status s msgs Pump pn OK else Open when PUMP STATE pn Open msgs pn chosen pumps s msgs Closed else Closed end The reasoning to predict the pump controller state is similar but we must take into account that two cycles may be needed before a just activated pump leads to a Flow state provided the pump is not stopped meanwhile Thus the next pump controller state is Unknown PCS if the next status of the Page 139 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 140 C Case Study The Steam Boiler Control System pump controller is not or if next_status of the corresponding pump is not OK otherwise the predicted pump controller state value is e Flow when the pump is not ordered to stop and it is currently Flow or it is currently NoFlow but PCS predicted SoonFlow e NoFlow if the pump is ordered to stop or if it is currently NoFlow and is not PCS predicted SoonFlow and the pump is not ordered to activate e SoonFlow otherwise This leads to the following PUMP CONTROLLER STATE PREDICTION spec ification spec PUMP CONTROLLER STATE PREDICTION DETECTION and then mert PCS predicted State x FinSet RR Message x PumpNumber ExtendedPump ControllerState Vs State msgs FinSet R Message pn PumpNumber e PCS predicted s msgs pn Unknown PCS when next status s msgs PumpController pn OK next_status s msgs
79. TATYPES booleans characters BASIC STRUCTUREDDATATYPES sets lists strings maps bags arrays trees BASIC GRAPHS directed graphs paths reachability connectedness coloura bility and planarity Basic ALGEBRA_II monoid and group actions on a space euclidean and factorial rings polynomials free monoids and free commutative monoids BAsic LINEARALGEBRA_I vector spaces bases and matrices BASIC LINEARALGEBRA II algebras over a field BASIC MACHINENUMBERS bounded subtypes of naturals and integers Page 225 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Does FTP also allow for artificial users 226 9 Libraries Libraries need not be registered for public access library http www brics dk pdm CASL Test Security from http casl passwordOwww brics dk pdm CASL RSA get KEY spec DECRYPT KEY then Libraries under development and libraries provided for restricted groups of users are named and accessed by their URLs This allows the CASL library constructs to be fully exploited for libraries that are not yet and perhaps never will be registered for public access Moreover validation of libraries can be a demanding and time consuming process and getting a library approved and registered is appropriate only when it provides specifications that are likely to be found useful by persons not directly involved it its development The primary Internet access protocols HTTP and FTP both support pass word pro
80. TRANSMISSION SYSTEM FAILURE then local Static analysis pred is static FinSet R Message Vmsgs FinSet RR Message e msgs is static OK lt gt junk msgs 310 Value e LEVEL v msgs Alu Value e STEAM v msgs Vpn PumpNumber e 3 ps PumpState e PUMP STATE pn ps msgs Vpn PumpNumber e 3 pcs PumpControllerState e PUMP_CONTROLLER_STATE pn pcs msgs Vpu PhysicalUnit e FAILURE ACKNOWLEDGEMENT pu msgs REPAIRED pu msgs 9596 Dynamic analysis pred is NOT dynamic OK for FinSet R Message x State Vs State msgs FinSet RR Message e msgs is NOT dynamic OK s lt mode s Initialization STEAM BOILER WAITING msgs V PHYSICAL UNITS READY e msgs V PhysicalUnit e FAILURE ACKNOWLEDGEMENT pu msgs status s pu OK V status s pu Failure WithAck V PhysicalUnit e REPAIRED pu e msgs status s pu OK V status s pu Failure WithoutAck within pred Transmission State x FinSet R Message Vs State msgs FinSet R Message e Transmission s msgs lt gt msgs is static msgs is NOT dynamic OK s end C 5 4 Detection of the Pump and Pump Controller Failures We start by considering the detection of the failures of the pumps As explained in Sec C 5 1 we rely on the predicted pump state message Thus in a first step we should extend the specificati
81. The water level measurement device The device to measure the level of water in the steam boiler provides the following information e the quantity q in litres of water in the steam boiler C 12 2 3 The pumps Each pump is characterized by the following elements Its capacity P in litres sec Its functioning mode on or off It s being started after having been switched on the pump needs five seconds to start pouring water into the boiler this is due to the fact that the pump does not balance instantaneously the pressure of the steam boiler e It s being stopped with instantaneous effect Page 150 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 12 The Steam Boiler Control Specification Problem 151 C 12 2 4 The pump control devices Each pump controller provides the following information e the water circulates from the pump to the steam boiler or in the contrary it does not circulate C 12 2 5 The steam measurement device The device to measure the quantity of steam which comes out of the steam boiler provides the following information e quantity of steam v in litres sec C 12 2 6 Summary of constants and variables The following table summarizes the various constants or physical variables of the system Unit Comment Quantity of water in the steam boiler C litre Maximal capacity litre Minimal limit litre Maximal limit litre Minimal normal No litre
82. _DEL Cowr DEL V 206 CONTAINER DEL_COMP 208 DEL_ComP1 202 FAILURE_DETECTION 111 110 203 FINSET FLAT_REQ GENERATEBAG GENERATEBINTREE 112 GENERATEBINTREE2 GENERATED_CONTAINER GENERATED_CONTAINER_MERGE GENERATED_SET GENERATEFINMAP GENERATEFINSET GENERATEKTREE 113 GENERATELIST GENERATENTREE 1113 GENERIC_COMMUTATIVE_MONOID GENERIC_COMMUTATIVE_MONOID_1 GENERIC_MONOID GENERIC MONOID 1 HOMOGENEOUS PAIR HOMOGENEOUS PAIR 1 IMPLIES DOES NOT HOLD INCONSISTENT 206 INT INTEGER INTEGER_ARITHMETIC INTEGER_ARITHMETIC_1 INTEGER_ARITHMETIC_ORDER INTEGER_AS_REVERSE_TOTAL_ORDER INTEGER_AS_TOTAL_ORDER 166 Index of Library and Specification Names KTREE LEVEL_FAILURE 1134 LIST LisT_AS_MONOID LIST_CHOOSE List_LENGTH List_LENGTH_NATURAL LisT ORDER LisT ORDER SORTED LisT ORDER SORTED 2 List_REV List_REV_NAT List REV ORDER Lisr REV WwrTH TWO ORDERS LisT REV WrrH TWO ORDERS 1 LisT_SELECTORS LisT_SELECTORS_1 LisT SELECTORS 2 LisT SET LisT SET 1 LisT WEIGHTED ELEM LisT WEIGHTED INSTANTIATED LisT WEIGHTED PAIR NATURAL COLOUR MARKING CONTAINER MAYBE 109 MESSAGE TRANSMISSION SYSTEM FAILURE 131 MESSAGES RECEIVED 119 MESSAGES SENT 119 MISTAKE MODE EVOLUTION MONOID MORE VEHICLE My_SYMBOL_TABLE AT_WORD AT WORD 1 AT WORD 2 ATURAL ATURAL ARITHMETIC ATURAL_ORDER ATURAL_ORDER_II ATURAL_PARTIAL_PRE ATURA
83. ad sort Node generated types Tree mktree Node Forest Forest empty add Tree Forest Here the mutually recursive datatypes Tree and Forest are correctly de fined simultaneously within the same generated types construct and the resulting semantics is the expected one without junk values for trees and forests Note that therefore the linear visibility rule is not applicable within a generated types construct to allow such mutually recursive definitions but that this is the only exception to the linear visibility principle Only mutually recursive generated datatypes need to be declared together in sim pler cases it makes no difference to have a sequence of successive generated datatype declarations or just one introducing all the desired datatypes 5 This can easily be fixed by replacing sort Node by sorts Node Tree Forest 6 The same explanations apply to free datatypes introduced in the next subsection Page 17 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 18 3 Total Many Sorted Specifications 3 3 Free Specifications Free specifications provide initial semantics and avoid the need for explicit negation spec NATURAL free type Nat 0 suc Nat end A free datatype declaration corresponds to the so called no junk no confusion principle there are no other values of sort Nat than those denoted by the constructor terms built with 0 and suc and all distinct constructor term
84. age x PhysicalUnit Dangerous WaterLevel State x FinSet R_Message given Snes STATE I local 9696 Auxiliary predicates to structure the specification of nert mode preds Everything OK Asked ToStop SystemStillControllable Emergency State x FinSet R Vs State msgs FinSet RR Message e Everything OK s msgs lt gt Transmission s msgs PhysicalUnit e PU_OK s msgs pu e AskedToStop s msgs lt gt nbSTOP s 2 STOP msgs e SystemStillControllable s msgs lt PU OK s msgs OutputOfSteam 3pn PumpNumber e PU s msgs Pump pn PU OK s msgs PumpController pn e Emergency s msgs mode s EmergencyStop V Asked ToStop s msgs V Transmission s msgs V Dangerous WaterLevel s msgs V PU OK s msgs WaterLevel SystemStillControllable s msgs within ops mode State x FinSet R Message Mode nezt nbSTOP State x FinSet R Message Nat Vs State msgs FinSet RR Message Emergency stop mode e Emergency s msgs gt next mode s msgs EmergencyStop 9696 Normal mode e Emergency s msgs Everything OK s msgs next mode s msgs Normal i e we must have a sequence of the form Normal Rescue Rescue gt Normal or Degraded in such cases Note that once in the EmergencyStop mode we specify that we stay in this mode forever rather than specifying that the steam boiler con
85. ailure e PUMP CONTROL FAILURE DETECTION n This message is sent un til receipt of the corresponding acknowledgement to indicate to the physi cal units that the program has detected a failure of the physical unit which controls a pump e LEVEL FAILURE DETECTION This message is sent until receipt of the corresponding acknowledgement to indicate to the physical units that the program has detected a failure of the water level measuring unit e STEAM FAILURE DETECTION This message is sent until receipt of the corresponding acknowledgement to indicate to the physical units that the program has detected a failure of the physical unit which measures the outcome of steam e PUMP REPAIRED ACKNOWLEDGEMENT n This message is sent by the program to acknowledge a message coming from the physical units and indicating that the corresponding pump has been repaired e PUMP_CONTROL_REPAIRED_ACKNOWLEDGEMENT n This mes sage is sent by the program to acknowledge a message coming from the physical units and indicating that the corresponding physical control unit has been repaired e LEVEL REPAIRED ACKNOWLEDGEMENT This message is sent by the program to acknowledge a message coming from the physical units and indicating that the water level measuring unit has been repaired e STEAM REPAIRED ACKNOWLEDGEMENT This message is sent by the program to acknowledge a message coming from the physical units and indicating that the unit which measures the outcome
86. akes haat den QUT das 49 LIST TERT re 50 NT 51 51 p PRA 51 52 eee ota nba 53 TEMP 53 LIST RDER SORTED 22 552 samo hada ERE 54 edu 58 59 60 61 160 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Named Specifications 161 ise dead wine hoe 61 Dole oe ween ae 61 61 2222 61 62 62 62 es acute 62 PEE 62 EE 63 ETT 63 IN LIE 63 ahead er ga T eee ane 64 piace ae he ee oe en ere 64 Tru 64 c 64 nee cce du LM 65 LisrT REV WITH TWO 5 65 MEE 66 hr c DEAE ILE I 67 METER 67 dd vdahde weed date E A a 67 fuk des ee tees te a 68 P 68 c PIC 68 Lisr REv 1 68 SML Kp 69
87. amming language Again the inductive definition style may be more suitable for pro totyping tools based on term rewriting while the observer definition style may be more suitable for theorem proving tools Sorts declared in free specifications are not necessarily generated by their constructors spec UNNATURAL free type UnNat 0 suc UnNat op 4 UnNat x UnNat UnNat assoc comm unit 0 Vz y UnNat e suc y suc z y Va UnNat e dy UnNat e x y 0 end This rather peculiar example illustrates the fact that a sort defined within a freeness constraint need not be generated by its constructors The unique up to isomorphism model of corresponds to integers and not Page 25 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 26 3 Total Many Sorted Specifications natural numbers as one may expect due to the last axiom This example points out why in general datatypes defined using freeness constraints can be more difficult to understand than datatypes defined using generatedness constraints However the reader should be aware that the specification uses a proper first order formula with an existential quantifier in the axioms The specification UNNATURAL is provided here for explanatory purposes only and clearly the writing of similar specifications should be dis couraged When only Horn clauses are used as axioms in a freeness constraint then the datatype will indeed be generated by its const
88. and repaired messages Thus in a first step we should extend the specification to add an observer related to the failure status of physical units spec SBCS STATE 2 SBCS STATE 1 then free type Status OK Failure WithoutAck Failure WithAck op status State x PhysicalUnit Status end Now the specification of how the status of a physical unit evolves i e of the operation next_status in is quite straightforward We rely again on the predicate PU OK 7 The reader may detect that the specification STATUS EVOLUTION is not totally correct However we prefer to give here the text of the specification as it was originally written and we will explain in Sec C 9 how we detect when validating the specification of the steam boiler control system that something is not correct and how the problem can be fixed Page 128 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 5 Specifying the Detection of Equipment Failures 129 spec STATUS_EVOLUTION pred PU OK State x FinSet R_Message x PhysicalUnit given Sacs STATE 2 op status State x F inSet R Message x PhysicalUnit Status Vs State msgs FinSet R Message PhysicalUnit e status s pu OK PU 5 msgs pu gt next_status s msgs OK e status s pu OK PU_OK s msgs gt next_status s msgs Failure WithoutAck e status s pu Failure WithoutAck FAILURE ACKNOWLEDGEMENT pu msgs gt next_statu
89. and Boat say sorts Amphibious lt Car Boat is impossible Subsorts may also arise as classifications of previously specified values and their values can be explicitly defined spec NATURAL SUBSORTS then pred even Nat e even 0 e even 1 Yn Nat even suc suc n lt even n sort Even x Nat e even x sort Prime 2 Nat e Vy z Nat e c yxz gt y 1Vz2 1 end The subsort definition sort Even 2 Nat even x is equivalent to the declaration of a subsort Even of Nat i e sorts Even Nat together with the assertion Vz Nat e x Even lt gt even z The main advantage of defining the subsort Even in addition to the predi cate even is that we may then use the subsort when declaring operations e g op times2 Nat Even and variables The subsort definition for Prime above illustrates that it is not always necessary to introduce and define an explicit predicate characterizing the val ues of the subsort the formula used in a subsort definition is not restricted to predicate applications In fact whenever a unary predicate p on a sort s could be defined by pred p x s f for some formula f we may instead define sort x e f and use sort membership assertions t P in stead of predicate applications p t avoiding the introduction of the predicate p altogether The following example is a further illustration of subsort definitions We declare a subsort Pos of Nat and
90. antics first defines mathematical entities that formally model the intended meaning of various concepts underlying CASL as already hinted at in Chap 2 and further introduced and discussed throughout the summary Part I The key concepts here are that of CASL signature model and formula together with the satisfaction relation between models and formulae over a common signature see Chaps 2 In fact these are variants of the standard algebraic and logical notions thus linking work on CASL to well established mathematical theories and ideas Page 88 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 11 Foundations 89 In a more or less standard way we use these concepts to build the semantic domains which the meanings of phrases in various syntactic categories of CASL inhabit We have chosen to give the semantics in the form of so called natural semantics with formal deduction rules to derive judgments concerning the meaning of each CASL phrase from the meanings of its constituent parts Not only is this a mathematically well established formalism with an unambiguous interpretation but we also hope that this makes the semantics itself more readable with details easier to follow than in some other approaches The overall semantics of CASL consists of two parts The static semantics captures a form of static analysis of CASL specifications in which they are checked for well formedness for example that axioms are well t
91. antics of INT consists of a signature and a class of models and is a self contained entity recall from Chap the models of a structured specification have no more structure than do those of a flat unstructured specification Thus downloading INT gives exactly the same re sult as if the reference to NAT in its text had been replaced by the text of For the same reason the presence of another item with the name NAT in the current library makes no difference to the result of downloading INT In terms of software packages downloading from CASL libraries is analogous to installing from binaries not from sources Downloading any item from another library B in a library A causes all the parsing and display annotations of B to be inserted at the beginning of A Conflicting annotations from different libraries are ignored altogether and local annotations override conflicting downloaded annotations The copied annotations allow terms to be written and displayed in A in the same way as in B Substantial libraries of basic datatypes are already available The organization of the following libraries of basic datatypes is explained in App BASIC NUMBERS natural numbers integers and rationals BAsIc RELATIONSANDORDERS reflexive symmetric and transitive rela tions equivalence relations partial and total orders boolean algebras BAsic ALGEBRA_1 monoids groups rings integral domains and fields BAsIC SIMPLEDA
92. apters and above it may still happen that when combining specifications this principle leads to unin tended name clashes An unintended name clash arises for instance when one combines two specifications that both export the same symbol with the same profile in case of an operation or a predicate while this symbol is not intended to denote the same thing in the combination In such cases it is necessary to explicitly rename some of the symbols exported by the specifications put together in order to avoid the unintended name clashes When reusing a named specification it may be convenient to rename some of its symbols moreover in the case of operation or predicate symbols one may also change the style of notation This is illustrated in the specifica tion STACK above which is obtained as a renaming of the specification LIST SELECTORS First the sort List is renamed into Stack then the operation cons is renamed into a mixfix operation push onto and finally the selec tors head and tail are renamed into top and pop respectively Note that r is input as gt The user only needs to indicate how symbols provided by the renamed specification are mapped to new symbols A signature morphism is auto matically deduced from this symbol map For instance the signature mor phism inferred from the symbol map specified in STACK maps the operation symbol cons Elem x List List to the operation symbol push onto
93. architectural specifications The following structured specifications will be referred to later in this chapter when illustrating CASL architectural specifications As defined in Chap 3 page 18 spec spec As defined in Chap a page 18 spec As defined in Chap page 20 spec ELEM sort Elem spec CoNT ELEM Similar to in Chap 3 page but with a compound sort Cont Elem generated type Cont Elem empty insert Elem Cont Elem pred _is_in__ Elem Cont Elem Ve e Elem Cont Elem e e is in empty e e is in insert e C e V e is in C end spec CoNT DEL ELEM Cor then op delete Elem x Cont Elem Cont Elem Ve e Elem Cont Elem e e is in delete e C e C e end Page 202 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 1 Architectural Specifications 203 spec Req Der NaTORAT spec FLAT_REQ free type Nat 0 suc Nat generated type Cont Elem empty insert Nat Cont Elem pred is in Nat x Cont Elem op delete Nat x Cont Elem Cont Elem Va y Nat Cont Elem e x is in empty e is in insert y C x y V is n C e is in delete y C C z y end 8 1 Architectural Specifications Let s assume in the following that REQ describes our requirements about the system to be implemented First note that both and F
94. are obviously compatible since their common symbols the sort Nat equipped with the operations 0 and suc all come from the same component N which provides their interpretation which is expanded hence cannot be modified in C N and in S N thus compatibility is guaranteed Open systems can be described by architectural specifications using generic unit expressions in the result part result AX ELEM e arch spec CONT2SET USED units N CSF arc spec ARCH_CONT2SET result CSF N So far our example architectural specifications have described closed stand alone systems where all components necessary to built the desired sys tem were declared in the architectural specification of interest In CASL it is however possible to describe open systems i e systems made of some com ponents that would require further components to provide a closed system This is illustrated by the architectural specification ARCH_CONT2SET which describes a system with a generic component implementing containers a generic component 5 implementing sets and a generic component that ex pands them to provide an implementation of the operation elements_of The result part is therefore a generic structured component 1 an open sys tem which given any component X implementing ELEM provides system built by applying F to the pair made of the applications of C to X and of S to X As illustrated by
95. arly for the water level first we compute the adjusted level interval which is either the interval reduced to the received level value if we rely on it i e if PU OK s msgs WaterLevel holds or the level_predicted interval stored in the state s at the previous cycle 4 Then we should consider broken pumps the pumps pn for which neither PU OK s msgs Pump pn PU_OK s msgs PumpController pn holds and the reliable pumps which are not broken and are therefore known to be either Open or Closed 5 At this point we must decide which pumps are ordered to activate or to stop However the specific control strategy for deciding which pumps should be activated or stopped need not to be detailed in this requirements specifica tion this can be left to a further refinement towards an implementation of the steam boiler control system Obviously the strategy should compare the adjusted level with the recommended interval N1 N2 and decide accordingly We will therefore rely on a loosely specified chosen pumps operation for which we just impose some soundness conditions e g a pump ordered to activate should be currently considered as reliable and Closed a pump ordered to stop should be currently considered as reliable and Open 6 Now we can compute the minimal and maximal amounts of water that will be poured into the steam boiler during the next cycle To compute minimal pumped water we consider that
96. as the expected carrier set but without any operation or predicate available on it Hiding the sort Nat in the specification see Chap 5 p may seem more appropriate but one should still note that the predicate lt is no longer available in ARITHMETIC hide sort Nat As a last remark note that when convenient reveal can be combined with a renaming of some of the exported symbols For instance in the above PARTIAL ORDER 2 specification we could have written reveal pred leq if in addition to a restriction of the signature of PARTIAL we wanted to rename the infix predicate __ lt _ into a predicate leq with a functional notation 6 4 Local Symbols Auxiliary symbols can be made local when they do not need to be ez ported spec LisT ORDER TOTAL ORDER with sort Elem pred _ lt then local op insert Elem x List List Ve e Elem L List e insert e empty cons e empty e insert e cons e D cons e insert e D when lt e else cons e cons e L within op order List List Ve Elem L List e order empty empty e order cons e L insert e order L end Page 52 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 6 4 Local Symbols 53 many cases auxiliary symbols are introduced for immediate use and they do not need to be exported by the specification where they are declared Then the best is to limit the scope of the declaratio
97. at we have some pumps some pump controllers and the two measuring devices Some messages have a value v as parameter From the informal require ments we can infer that these values are approximations of real numbers but indeed it is not necessary at this level to make any decision about the exact specification of these values In our case study we will therefore rely on a very abstract loose specification VALUE introducing a sort Value together with some operations and predicates which are left unspecified we expect of course that these operations and predicates will have the intuitive inter pretation suggested by their names This means that we consider VALUE as being a general parameter of our specification This point is discussed again in Sec Note also that we will abstract from measuring units such as litre litre sec since ensuring that these units are consistently used is a very minor aspect of this particular case study This first analysis leads to the following specifications and MESSAGES RECEIVED from BASiC NUMBERS get NAT spec VALUE 9696 At this level we don t care about the exact specification of values NAT then sorts Nat Value ops 0 1 Nat Value x Value Value assoc comm unit 0 Value x Value Value X Value x Value Value assoc comm unit 1 2 Value Value min maz Value x Value Value preds _ lt lt __ Value x Value end
98. axioms of the specification to Isabelle s simplifier a rewriting engine Note that here we rely on the axioms being terminating To prove the first property expressed by the view we first have to type in the goal Then we chose to induct over the variable and the rest can be done with automatic simplification Finally we name the theorem for later reference Goal forall x Nat not x lt x by induct tac x 1 by Auto tac qed Nat irreflexive Both Hets and also provide an interface to HOL CASL such that proof obligations arising in development graphs can be discharged using HOL CASL Page 82 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 4 ELAN CASL 83 10 4 ELAN CASL ELAN CASL is rewriting engine for the Horn sublanguage CASL _ Is this correct Or is it FOL without ELAN CasL R00 is based on a translation of the Horn sublanguage quantifiers CASL to the input language of the rewriting engine ELAN It can be obtained under http www loria fr equipes protheo SO0FTWARES ELAN The required inputs for ELAN are e A rewrite program including a signature a set of rules and a set of strate gies e query term expressed in the signature of the rewrite program The ELAN outputs are the normal forms of the query term with respect to the rewrite program Note that because the set of rules is not required to be terminating nor confluent a query term may have several
99. b tasks Thus architectural specifications are essential at the design stage where the focus is on how to factor the imple mentation of the system into components glued together The aim of this chapter is to discuss and illustrate both the r le of archi tectural specifications and how to express them in CASL 202 8 Specifying Architectural Structure The idea underlying architectural specifications is that eventually in the process of systematic development of modular software from specifications components are implemented as software modules in some chosen program ming language However this step is beyond the scope of specification for malisms so in CASL and in this chapter we identify components with models and with functions from models to models in the case of generic components The modular structure of the software under development as described by an architectural specification is therefore captured here simply as an explicit structural way to build CASL models The illustrations in this chapter are artificially simple Architectural specifications and more generally component oriented ap proaches are intended for relatively large systems In this chapter however we have to rely on simple small examples to illustrate and explain CASL ar chitectural specification concepts and constructs After reading this chapter the reader is encouraged to study which provides realistic examples of the use of
100. be installed on the Internet for remote access library BAsic NUMBERS left_assoc _ _ Y number _ _ floating E lt spec NAT free type Nat 0 suc Nat ops 1 Nat suc 0 9 Nat suc 8 _ _ m n Nat Nat x suc 9 n spec INT Nart then spec RAT INT then spec DECIMALFRACTION RAT then ops Nat x Nat Rat E Rat x Int Rat The above example is an extract from one of the CASL libraries of basic datatypes described in App Bland available on the Internet It illustrates the overall structure of a library intended for general use as well as some helpful annotations concerning literal syntax for numbers which are explained below CASL libraries are identified by hierarchical path names For instance all the CASL libraries of basic datatypes have names starting with BAsIc and path names starting with CASL are reserved for libraries connected with the CASL language itself e g the specification of the abstract syntax of CASL in CASL COFI is to maintain a register of validated libraries The validation of a library ensures not only that it is well formed but also that the specifica tions and views are consistent and that all proof obligations corresponding to semantic annotations in the library have been verified Moreover some methodological guidelines concerning the style of names have been provided to facilitate t
101. ble and we can only use our intuition to assess the well foundedness of the interpretations made during the writing of the formal specification 2 Once a validated requirements specification is obtained we can proceed Is a pointer to Mos03 Part V needed here toward a program by a sequence of refinements Here a crucial step is the choice of an architecture of the desired implementation expressed by an architectural specification as explained in Chap 8 Each refinement step leads to proof obligations which allow the correctness of the performed refinement to be assessed In a last step a program is derived from the final design specification Before starting to explain how to write a CASL requirements specifica tion of the steam boiler control system let us make a few comments on this case study First note that although in principle a hybrid system the steam Page 116 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 2 Getting Started 117 boiler control system turns out to be merely a reactive not even a hard real time system see e g the assumptions made in Sec 3 Moreover even if the whole system i e the control program and its physical environ ment is distributed this is not the case at least at the requirements level for the steam boiler control system CASL turns out to be especially well suited to capture the features of systems like the steam boiler control system where data and control are equally impor
102. c Library given INT sort Index i Int e min lt i i maz then sort Index fit sort S Index sort Elem fit sort T Elem with sort FinMap Index Elem gt Array Elem op empty init then ops l Array Elem x Index x Elem Array Elem _ __ Array Elem x Index gt Elem reveal sort Array Elem ops init 1 _ _ _ end spec GENERATEBINTREE sort Elem free type BinTree Elem nil bin Tree entry Elem left Bin Tree Elem right BinTree Elem end spec BINTREE sort Elem given NAT GENERATEBINTREE sort Elem and FINSET sort Elem then preds isEmpty isLeaf Bin Tree Elem isCompound Tree BinTree Elem Elem x BinTree Elem ops height BinTree Elem Nat leaves BinTree Elem FinSet Elem end spec GENERATEBINTREE2 sort Elem mono free type NonEmptyBinTree2 Elem leaf entry Elem bin Tree left NonEmptyBinTree2 Elem right NonEmptyBin Tree2 Elem free type BinTree2 Elem nil sort NonEmptyBin Tree2 Elem end spec BINTREE2 sort Elem given NAT mono GENERATEBINTREE2 sort Elem and FINSET sort Elem then def Page 112 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 B 2 Library Basic StructuredDatatypes 113 preds isEmpty isLeaf BinTree Elem isCompoundTree Bin Tree2 Elem 6 Elem x 2 Elem ops height BinTree2 Elem Nat leaves BinTree2 Elem FinSet Elem
103. ce there is no easy way to infer when z y is defined From a methodological point of view the following alternative version is much better spec NATURAL PARTIAL SUBTRACTION 1 then op Nat x Nat Nat y Nat e def r y e y zVy za 0 e suc y pre z y end The above examples clearly demonstrate why the explicit specification of definition domains is generally advisable from a methodological point of view However they also indicate that this recommendation should not be applied in too strict a way and that deciding whether a specification is explicit enough or not is to some extent a matter of taste Partial functions are minimally defined by default in free specifica tions spec LIsT_SELECTORS_1 sort Elem sort Elem then free ops head List gt Elem tail List List Ve Elem L List e head cons e L e e tail cons e L L end In the above example the given axioms imply that head and tail are de fined on lists of the form cons e L The freeness constraint implies that these functions are minimally defined Since the terms head empty and tail empty are not equated to any other term the freeness constraint implies that these terms are undefined and hence that the functions head and tail are unde fined on empty The situation here is similar to the fact that predicates hold minimally in models of free specifications see Chap 3 p 19
104. clear as possible by referring to simple examples and by discussing both the general ideas and some details of CASL specifications We hope that this has given the reader a sufficient feel of the formalism and enough understanding to look through the presentation of a basic library of CASL specifications in App to follow the case study in App and to start experimenting with the use of CASL for writing specifications perhaps employing the support tools presented in Chap By no means however should this User Manual be regarded as a com plete presentation of the CASL specification formalism this is given in the accompanying volume the CAsL Reference Manual Mos03 CASL has a definitive summary Part I of the CASL Reference Manual offers a definitive summary of the en tire CASL language all the language constructs are listed there systematically together with the syntax used to write them down and a detailed explanation of their intended meaning However although it tries to be precise and com plete the CASL Summary still relies on natural language to present CASL 88 11 Foundations This inherently leaves some room for interpretation and ambiguity in vari ous corners of the language for example where details of different constructs interact CASL has a complete formal definition key aim of the entire initiative is to avoid any potential ambi guities by providing a complete formal d
105. composition of generic specifications is fairly easy in CASL Note however that this composition is achieved by means of appropriate instantiations some possibly trivial and that CASL does not provide higher order genericity in its current version end 7 2 Compound Symbols Compound sorts introduced by a generic specification get automatically renamed on instantiation which avoids name clashes However the situation would be different if the parameter of GENERATED_SET would have been e g sort Val since then the absence of an explicit fitting symbol map would have led to an ambiguity in that case the specifier would have been forced to specify whether the sort Val is to be mapped to Elem or to List Page 63 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 64 7 Generic Specifications spec LIST_REV sort Elem free type List Elem empty cons head Elem tail List Elem ops List Elem x List Elem List Elem assoc unit empty reverse List Elem gt List Elem Ve Elem L L1 L2 List Elem e cons e L1 L2 cons e L1 L2 e reverse empty empty e reverse cons e L reverse L e end spec LisT REV NAT List_REV NATURAL end In the specification LisT REV we introduce a compound sort List Elem to denote lists of arbitrary elements When the specification LisT REV is instantiated as in the translation induced by the implicit fitting symbol
106. constraint may be unavoidable to define a predicate as ilustrated by the choice between relying on a free ness constraint to define a datatype such as Set or using instead a generated datatype declaration together with some observers to unambiguously deter mine the values of interest is largely a matter of convenience One may argue that SET is more suitable for prototyping tools based on term rewriting while SET GENERATED is more suitable for theorem proving tools The def annotation is useful to indicate that some operations or predicates are uniquely defined spec SET_UNION sort Elem sort Elem then def ops _U_ Set x Set Set assoc comm idem unit empty remove Elem x Set Set Ve Elem 8 5 Set S U insert e S insert e S U S remove e empty empty remove e insert e remove e S remove e insert e insert e remove e S if end The annotation def expresses that SET_UNIONiis a definitional extension of SET i e that each model of can be uniquely extended to a model of which means that the operations introduced in SET_UNION are uniquely defined As the implies annotation the def annotation has no impact on the semantics but merely provides useful proof obligations The def annotation is especially useful to stress that the specifier s intention is to impose a unique interpretation of what is defined within the scope of this annotatio
107. constructors are frequently needed CASL provides special constructs for datatype declarations to abbreviate the corre sponding rather tedious declarations For instance the above datatype decla ration type Container empty insert Elem Container abbreviates sort Container ops empty Container insert Elem x Container Container A datatype declaration looks like a context free grammar in a variant of BNF It declares the symbols on the left of as sorts and for each alternative on the right it declares a constructor A datatype declaration as the one above is loose since it does not imply any constraint on the values of the declared sorts there may be some values of sort Container that are not built by any of the declared constructors and the same value may be built by different applications of the constructors to some arguments For instance depending on the context the term t1 12 can be disambiguated by writing Monoid x Monoid Monoid t1 12 or just 21 Monoid x t2 Monoid or even t1 x 12 Monoid Page 13 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 14 3 Total Many Sorted Specifications Datatype declarations may also be specified as generated see Sect or free see Sect 3 3 Moreover selectors which are usually partial operations may be specified for each component see Chap As a last minor remark note that while placeholders are specified with pairs of underscore
108. control system should stay in the same operating mode or switch to another one However things get simpler if we analyze under which conditions the next mode is one of the specified operating modes In particular a careful analysis of the requirements shows that except for switching to the EmergencyStop mode we can determine the new operating mode after receiving some messages without even taking into account the previous one To improve the legibility of our specification it is better to introduce some auxiliary predicates Everything OK AskedToSop SystemStillControllable It is important to make a subtle distinction between the actual failures about which we basically know nothing and the failures detected by the steam boiler control system In our specification the behaviour of the steam boiler control system is induced by the failures detected whatever the actual failures are Page 123 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 124 C Case Study The Steam Boiler Control System and Emergency that will facilitate the characterization of the conditions un der which the system switches from one mode to another 5 If our interpretation is incorrect then in some cases we may have replaced The aim of the predicate Everything_OK is to express that we believe that all physical units operate correctly including the message transmission system The aim of the predicate AskedToSop is to determine if we have received the STOP
109. ctly the domain of definition of choose but does this too implicitly since some reasoning is needed to con clude that the above specification entails def choose S 8 empty To improve the clarity of specifications it is in general advisable to specify definition domains as explicitly as possible and is somehow easier to understand than a tions define the same class of models spec NATURAL PARTIAL then op pre Nat Nat Nat e def pre 0 e pre suc z x end In the above example one can consider that the domain of definition of pre is exactly specified in an explicit enough way since the first axiom states exactly that pre 0 is undefined while the second one implies that pre is defined for all natural numbers of the form suc x In this example it is essential to choose a new name for our partial addi tion operation Otherwise since is rightly declared as a total operation in the declaration op __ _ Nat x Nat Nat would be useless the same name same thing principle would lead to models with just one total addition operation Page 31 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 32 4 Partial Functions spec NATURAL PARTIAL SUBTRACTION then op Nat x Nat Nat y Nat 0 e suc y pre z y end The above specification is perfect from a mathematical point of view but is clearly not explicit enough sin
110. cture of the Steam Boiler Control System We now have a validated requirements specification L SYSTEM of the steam boiler control system The next step is to refine it into an architectural specification thereby prescribing the intended architecture of the implementation of the steam boiler control system Indeed the expla nations given in Sec C 3 suggest the following rather obvious architecture for the steam boiler control system arch spec ARCH SBCS units P VALUE gt 8 P SBcs_STATE See ST Recs ETS Spcs_ANALYSIS gt TEAM_BOILER_CONTROL_SYSTEM Note that we decide to describe the implementation of the steam boiler control system as an open system relying on an external component V imple menting VALUE This is consistent with our explanations in Sec choosing a specific implementation of VALUE is obviously orthogonal to designing the implementation of the steam boiler control system This means in particu lar that the component V implementing VALUE will encapsulate the chosen representation of natural numbers and values together with operations and predicates operating on them In a next step we can refine the specification VALUE PRELIMINARY of the component P into the following architectural specification arch spec ARCH PRELIMINARY units SET sort Elem x NAT FINSET sort Elem MS MR VALUE MESSAGES RECEIVED given CST resul
111. cy observed by the operation freq for all entries Lists are specified in terms of a free datatype In the specification GEN ERATELIST lists are built up from the empty list by adding elements in front The usual list operations are provided first and last select the first or last element of a list while rest or front select the remaining list ZZ counts the number of elements in a list take takes the first n elements of a list while drop drops them The specification ARRAY includes the condition min lt maz as an axiom in its first parameter This ensures a non empty index set Arrays are defined as finite maps from the sort Index to the sort Elem where the typical array operations evaluation and assignment are introduced in terms of finite map operations Finally revealing the essential signature elements yields the desired datatype The library concludes with several specifications concerning trees There are specifications covering binary trees BINTREE BINTREE2 k branching trees KTREE and trees with a possibly different branching at each node NTREE Each of these branching structures can be equipped with data in different ways Either all nodes of a tree carry data as it is the case in BIN TREE KTREE and NTREE or just the leaves of a tree have a data entry as in BINTREE2 library BASIC STRUCTUREDDATATYPES from Basic NUMBERS version 1 0 get INT spec MAYBE sort S mono free type Maybe S L jus
112. d by its subsorts spec VEHICLE then sorts Car Bicycle Vehicle Ops maz speed Vehicle Nat weight Vehicle Nat engine capacity Car Nat end The above example introduces three sorts Car Bicycle and Vehicle and declares both Car and Bicycle to be subsorts of Vehicle A subsort declaration entails that any term of a subsort is also a term of the supersort so here any term of sort Car is also a term of sort Vehicle and we can apply the operations max speed and weight to it and similarly for a term of sort Bicycle In other words with the single declaration maz speed Vehicle Nat we get the effect of having declared also two other operations maz speed Car Nat and speed Bicycle gt Obviously operations that are only meaningful for some subsort should be defined at the appropriate level This is the case here for the operation engine_capacity which is only relevant for cars and therefore defined with the appropriate profile exploiting the subsort Car Inheritance applies also for subsorts that are declared afterwards spec MORE_VEHICLE VEHICLE then sorts Boat lt Vehicle end 1 Strictly speaking there is just speed operation in the signature of Page 38 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 5 1 Subsort Declarations and Definitions 39 The order in which a subsort and an operation on the supersort are de clared is irrelevant
113. d specifications in CASL may be written essentially as in many other algebraic specification languages The simplest kind of algebraic specification is when each specified opera tion is to be interpreted as an ordinary total mathematical function it takes values of particular types as arguments and always returns a well defined value Total functions correspond to software whose execution always termi nates normally The types of values are distinguished by simple symbols called sorts In practice a realistic software specification involves partial as well as total functions However it may well be formed from simpler specifications some of which involve only total functions This chapter explains how to express such total specifications in CASL illustrating various features of CASL Total many sorted specifications can also be expressed in many previous specification languages it is usually straightforward to reformulate them in CASL Readers who know other specification languages will probably recognize some familiar examples among the illustrations given in this chapter CASL provides also useful abbreviations The technique of algebraic specification by axioms is generally well suited to expressing properties of functions However when functions have commonly occurring mathematical properties it can be tedious to give the corresponding axioms explicitly CASL provides some useful abbreviations for such cases For ins
114. datatypes B 1 Library Basic Numbers This library provides monomorphic specifications of natural numbers inte gers rational numbers and rational numbers In the specification NAT the natural numbers are specified as a free type together with a bunch of predicates and operations over the sort Nat of natural numbers Note that the names for the partial operations subtraction and division __ __ include a question mark This is to avoid overloading with the total operations __ __ on integers and __ __ on rationals which would lead to Possibly also in the CD coming with this user manual if there is one 106 B Basic Library RelationsAndOrdes gt Algebra_I aa SimpleDatatypes MachineNumbers C Smcuredbuatypes gt Algebra LinearAlgebra I LinearAlgebra II Fig B 1 Dependency graph of the libraries of basic datatypes inconsistencies as both these specifications import the specification of natural numbers The introduction of the subsort Pos consisting of the positive naturals gives rise to certain new operations e g Pos x Pos Pos whose semantics is completely determined by overloading The specification INT of integers is built on top of the specification of naturals integers are defined as equivalence classes of pairs of naturals written as differences the axioms which are omitted in the specification below Page 106 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 B 1 Lib
115. defined and the strong equation holds trivially 1 Note that the term choose empty is well formed and therefore is a correct term It is its value which may be undefined To avoid unnecessary pedantry in the following we will simply write that a term is undefined to mean that its value is so Obviously a term with variables may be defined for some values of the variables and undefined for other values Page 28 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 4 2 Specifying Domains of Definition 29 CASL provides also so called existential equations explained at the end of this chapter Special care is needed in specifications involving partial functions Partial functions are intrinsically more difficult to understand and specify than total ones This is why special care is needed when writing the axioms of specifications involving partial functions The point is that an axiom may imply the definedness of terms containing partial functions and as a conse quence that these functions are total which may not be what the specifier intended There are three typical cases of such situations Asserting choose S is in 5 as an axiom implies that choose is defined for any S The point here is that since predicates applied to an undefined term do not hold in any model satisfying choose S is in S the function choose must be total i e always defined Asserting remove choose S insert choose S empty
116. does indeed denote a value but the value is not a positive natural number so the value of the term pre pre suc 1 as Pos as Pos is undefined Note that def t as s is equivalent to t s for a well formed term t of a supersort of s Overloading a total cons on List with a partial cons on the subsort OrderedList would either lead to a total cons operation on OrderedList or to an inconsis tent specification depending on how the definition domain of the partial cons is specified Page 43 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 44 5 Subsorting Supersorts may be useful when generalizing previously specified sorts spec INTEGER_ARITHMETIC_1 then free type Int sort Nat _ Pos Ops _ Int x nt Int assoc comm unit 0 _ Int x Int Int Int x Int Int assoc comm unit 1 abs Int Nat Int n Nat p q Pos e suc n 1 n e suc n suc q n 4 e 2 er 0 z 1 4 1 4 e nx q n q e p q p q e abs n n e abs p p end The specification extends and defines the sort nt as a supersort of the sort Nat As a consequence terms which have two parses in sort Int such as suc 0 are required by the semantics of subsorting to have the same value for both parses and they can therefore be used without explicit disambiguation The situation would be quite different if
117. e 64 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 7 2 Compound Symbols 65 Since the specification provides three sorts Nat Pos and Int an explicit fitting symbol map is needed in the above instantia tions which provide the sorts List Nat and List Int Note that the subsorting relation Nat lt Int does not entail List Nat lt List Int but of course this can be added if desired in an extension by a subsorting declaration Compound symbols can also be used for operations and predicates spec Lisr REV ORDER TOTAL ORDER sort Elem then local op insert Elem x List Elem List Elem Ve e Elem L List Elem e insert e empty cons e empty e insert e cons e L cons e insert e D when e e else cons e cons e L within op order lt List Elem List Elem Ve Elem L List Elem e order __ lt _ empty empty e order lt _ cons e L insert e order __ lt L end spec LIST_REV_WITH_ TWO_ORDERS INTEGER_ARITHMBTIC_ORDER fit gt gt Int lt gt lt Provides the sort List Int and the operation order __ lt __ and INTEGHR_ARITHMMETIC_ORDER fit Elem gt Int lt gt Provides the sort List Int and the operation order __ gt then implies VL List Int e order lt _ L reverse order gt L end The above example illustrates the use of compound identifiers for operation symbols and the same rules appl
118. e empty is_sorted e cons e cons e L is_sorted cons e L is_sorted e lt e within op order List SortedList end Page 53 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 54 6 Structuring Specifications Note that the above specification WRONG_LIST ORDER_SORTED which may at first glance be considered as a slight variant of is illegal order is exported by WRONG_LIST_ORDER_SORTED and hence all sorts occurring in its profile should also be exported which cannot be since the sort SortedList is auxiliary So if the specifier really intends to insist that the result sort of order is SortedList this subsort should be exported as shown below spec LIST_ORDER_SORTED_2 TOTAL_ORDER with sort Elem pred _ lt __ sort Elem then local pred is sorted List Ve e Elem L List e empty is sorted e cons e empty is_sorted e cons e cons e L is_sorted cons e L is sorted e lt e within sort SortedList L List e is_sorted L op order List SortedList end In fact the local within construct abbreviates a combination of extension and explicit hiding In Lisr ORDER SORTED 2 above for instance it abbreviates 1 pred _is_sorted List Ve e Elem L List e empty is sorted e cons e empty is_sorted e cons e cons e L is_sorted cons e L is sorted e lt e then sort SortedList L List e is_sorted L op order List SortedList j hide 15
119. e E cote A 120 SBCS_DTATE ll idu br Reb ed pues vs 122 Dicen esL 125 SBCS 5 TATE 2 cn PE AE c lb ane dle ead ees 128 PT 129 Jor 131 SBGS STATE 22505 Cand scr bbe kis EP Pd dd 132 132 Bad Ede bb eb P d peau YS 132 MI 133 SBCS S TATE 5 fog dakar dhe e date a pede qe rd pese us 133 134 C 134 134 Page 162 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Named Specifications 163 oN 137 EMT 139 22005 140 rx 140 SBCS_ANALYSISE 2555 S Es deditus 141 Terr 142 rre 142 nr 145 TTE 145 E 146 dd d bea ADR D dee da rA Opa eed OE 147 P 147 A ee es 148 Page 163 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Index of Library and Specification Names ANOTHER WELL STRUCTURED ARCH gt gt gt gt gt gt gt gt gt BADLY_STRUCTURED_ARCH_SPEC BAG BASICS SPEC 215 RCH_ANALYSIS 147 RCH CoNT2SET 212 RCH_CONT2SET_NAT 211 RCH_CONT2SET_NAT_V RCH_CONT2SET_USED 212 RCH_FAILURE_DETECTION RCH_PREDICTION RCH PRELIMINARY RCH SBCS 1145 214 111 119 BINTREE BINTREE2 COLOUR CONT CONT2SET CONT_COMP 202 211 208 ContT
120. e actions should be taken corresponding to the messages to be sent to the environment State variables are also updated according to the result of the analysis of the received messages and the messages to be sent e Finally a specification describes the overall control command system as a labeled transition system A very rough preliminary sketch of the steam boiler control system speci fication looks therefore as follows library SBCS from Basic NUMBERS get from Basic STRUCTUREDDATATYPES get FINSET 9696 Display annotations for half and square to be added here spec spec then end spec then end Page PRELIMINARY 4 See previous section 96 SBCS STATE sort State ops 9696 Needed state observers are introduced here 9696 E g we need an observer for the mode of operation mode State Mode SBCS ANALYSIS SBCS STATE 9696 Analysis of received messages and in particular failure detection 9696 Computation of the messages to be sent op messages to send State x FinSet R Message gt F inSet S Message 9696 Computation of the updates of the state variables 4 For each observer obs defined in SBCS STATE we introduce an operation next_obs that computes the corresponding update according to the analysis of the messages received in this round For instance we specify here an operation next mode corresponding to the update of the observer mode Y 96 ops nert mode State x FinSet
121. e equivalent to their union For instance the above PAIR specification could as well have been defined as follows spec PaAIR 1 sorts Elem2 Note that writing spec HOMOGENEOUS PAIR 1 sort Elem sort Elem free type Pair pair first Elem second Elem end merely defines pairs of values of the same sort and is equivalent to and better defined as follows spec HOMOGENEOUS_PaIR sort Elem free type Pair pair first Elem second Elem end since the two parameters HOMOGENEOUS PAIR 1 are equivalent to just one sort Elem parameter From a methodological point of view it is generally advisable to use as many parameters as convenient the part of the specification that is intended to be specialized at instantiation time is better split into logically coherent units each one corresponding to a parameter Consider for instance spec SYMBOL TABLE sort Symbol sort Attribute Here using two parameters in SYMBOL TABLE emphasizes that Symbol and Attribute are logically distinct entities which can be specialized as desired independently of each other Instantiation of generic specifications with several parameters is sim ilar to the case of just one parameter spec PAIR NATURAL COLOUR NATURAL ARITHMETIO COLOUR At Elem gt RGB end In the above example the first parameter sort Elem1 of PAIR is instan tiated by which exports only one sort Nat hence no ex
122. e try to make these points as clear as possible by referring to simple examples and by discussing both the general ideas and some details of CASL specifications We hope that this will give the reader a sufficient feel of the formalism and enough understanding to look through the presentation of a basic library of CASL specifications in App to follow the case study in App and to VI Preface start experimenting with the use of CASL for writing specifications perhaps employing the support tools presented in Chap By no means however should this User Manual be regarded as a com plete presentation of the CASL specification formalism this is given in the accompanying volume the CasL Reference Manual Mos03 Structure Chapter 1 describes the origins of CASL how was formed in response to the proliferation of algebraic specification languages in the preceding two decades and the aims and scope that were formulated for this international initiative For the benefit of readers not already familiar with other algebraic spec ification languages Chap 2 will review the main concepts of algebraic spec ification explaining standard terminology regarding specification language constructs and models i e algebras Chapter 3 shows how total many sorted specifications in CASL may be written essentially as in many other algebraic specification languages Loose generated and free specifications are discussed in tur
123. ecification Names 167 STEAM FAILURE 1134 STRICT PARTIAL ORDER 6 STRUCTUREDDATATYPES SYMBOL TABLE SvsrEM 203 SvsTEM 1 SvsTEM G 206 SvsTEM G1 SvsTEM V TOTAL ORDER TOTAL ORDER WiTH MINMAX RANSITIVE CLOSURE Two_Lists Two_Lists_1 UNNATURAL vl v2 VALUE 118 VARIANT_OF_TOTAL_ORDER_WITH_ MINMAX VEHICLE WELL_STRUCTURED_ARCH_SPEC 215 WRONG_ARCH_SPEC 214 WRONG_LIST_ORDER_SORTED 17 Sep 2003 17 54
124. ecifications Chap III 5 which relies on a formal counterpart of the concept of a unit module of a system to be developed self contained units are viewed simply as models of the underlying institution and parametrized units as functions mapping such parameter models to result models Architectural specifications provide a way of specifying the component units of a system and indicating how the overall Page 89 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 90 11 Foundations system is built by putting these units together This intuition is captured by the semantics of architectural specifications which denote a class of permitted unit bindings and a function that maps each such environment to a result unit Finally the libraries layer of CASL is given a rather standard description with libraries modeled as environments giving names to the entities introduced specifications architectural specifications etc see Chap III 6 The semantics is the ultimate reference for the meanings of all CASL constructs Overall the formal mathematical semantics is crucial in the understanding of CASL specifications It provides their unambiguous meaning and thus gives the ultimate reference point for all questions concerning the interpretation of any CASL phrase in any context We have already experienced how important such a formal semantics may be in the design of CASL itself In many cases the intended semantics was prominent in inter
125. ed on joint work with Markus Roggenbach and Lutz Schr der Chapter 11 was written by Donald Sannella and Andrzej Tarlecki Comments on previous drafts of Chaps 13561 from CoFI participants have been very helpful Draft Status Many of the main chapters are close to a final draft However some of the less central chapters Chaps and 9 have been given lower priority and are still at the outline stage A full draft of Chapter 8 is expected to become available by the beginning of August followed by Appendix We look forward to all comments based on the present draft of the User Manual either addressed personally to the authors or preferably submitted to the moderated discussion mailing list cofi discuss cofi info Michel Bidoit and Peter D Mosses 15 July 2003 Page VIII FIRST PUBLIC DRAFT 17 8ep 2003 17 54 Contents 1 EL ECC EF DAR 1 eps hie Sahat aud Aenea au ata ear 1 2 Underlying Concepts 3 2 1 ete bees 3 2 2 Algebras ch eased ence ERE QE 3 5 en eee 6 15 ETA T 18 4 Partial Functions 27 pie tel da edi 27 DER 29 4 3 Partial Selectors and
126. ed to indicate which items have changed between two versions of a library Libraries can refer to specific versions of other libraries library BAsIC STRUCTUREDDATATYPES version 1 0 from Basic NUMBERS version 1 0 get INT spec LIST sort Elem given NAT spec ARRAY given INT Downloading items from particular versions of libraries is necessary if one wants to ensure coherence between libraries For example as illustrated above version 1 0 of BASIC STRUCTUREDDATATYPES downloads NAT and INT from version 1 0 of BAstc NUMBERS Omitting the version number when down loading gives implicitly the current version of the library which may of course change Even though the developers of libraries may try to ensure backwards compatibility between versions it could happen that symbols introduced in a new version of a downloaded specification clash with symbols already in use in the library that specified the downloading causing ill formedness or incon sistency So for safety it is advisable to give explicit version numbers when downloading also when downloading from version 0 of another library If one subsequently wants to use symbols that are introduced only in some later version of another library all that is needed is to change the version number in the downloading s An alternative strategy is to ensure consistency with the current versions of all libraries from which specifications are downloaded by observing
127. ed to the same non generic component but only to two applications of the same generic component A to similar arguments It is advisable to use unit terms where compatibility can be checked by a simple static analysis CASL provides additional constructs which make it easy to follow this recommendation as explained below Page 214 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 3 Writing Meaningful Architectural Specifications 215 Auxiliary unit definitions or local unit definitions may be used to avoid repetition of generic unit applications arch spec WELL_STRUCTURED_ARCH_SPEC units N NATURAL A Reroran Nerunar AN AJN 5 F x GenenaTED Ser Eren LEM result F C AN S A arch spec ANOTHER_WELL_STRUCTURED_ARCH_SPEC units N A S F result local AN A N S AN The problem illustrated in can be fixed easily An auxiliary unit definition may be used to avoid the repetition of some generic unit applications such as AN A N in WELL_STRUCTURED_ An alternative is to make the definition of AN local to the re sult unit term as illustrated in In both case common symbols can be traced to a non generic unit and com patibility can be checked by an easy static analysis Page 215 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 9 Libraries Libraries are named collections of named specifications In the fo
128. eferenced specification can be adjusted through appropri ate combinations of renaming and hiding although this should not often be necessary provided that auxiliary symbols are made local as explained in the previous section Page 55 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 7 Generic Specifications Making a specification generic when appropriate improves its reusability As mentioned in the previous chapter naming specifications is a good idea In many cases however datatypes are naturally generic having sorts operations and or predicates that are deliberately left loosely specified to be determined when the datatype is used For instance datatypes of lists and sets are generic regarding the sort of elements Generic specifications allow the genericity of a datatype to be made explicit by declaring parameters when the specification is named in the case of lists and sets there is a single parameter that simply declares the sort A fitting argument specification has to be provided for each parameter of a generic specification whenever it is referenced this is called instantiation of the generic specification The aim of this chapter is to discuss and illustrate how to define generic specifications and instantiate them We have seen plenty of simple examples of generic specifications and instantiations in the previous chapters In more complicated cases however explicit fitting symbol maps may be requi
129. efinition for CASL and sound math ematical foundations for the advocated methodology of its use in software specification and development Abstract and concrete syntax of CASL are defined formally We begin by giving a formal definition of the syntax of CASL in Part II of the Reference Manual Abstract syntax is given where each phrase is written in a way that directly indicates its components thus making evident its inter nal structure In essence the use of each construct of the language is explicitly labeled here This is convenient for formal manipulation and analysis but is not so readable Therefore the so called concrete syntax of CASL as used for instance in the examples throughout this User Manual is given as well retaining a direct correspondence with the abstract syntax This offers to the user of CASL a convenient and readable way of writing down CASL specifi cations in a way that makes clear the formal structure of the phrases and constructs used to build them As usual the syntax is given as a context free grammar using a variant of the BNF notation relying on well established theory to give its formal meaning and on a variety of tools and techniques available for syntactic analysis of languages presented in such a style CASL has a complete formal semantics The ultimate definition of the meaning of CASL specifications is provided by the semantics of CASL in Part III of the Reference Manual The sem
130. em Nat Ve Elem L List Elem e length empty 0 e length cons e L length L 1 then implies VL List Elem e length reverse L length L end The specification LIst_LENGTH needs the sort Nat and the usual arith metic operations provided by to specify the length operation In this case it is clear that the given part has nothing to do with the trivial parameter of The reason to specify as a given fixed part is that this will make instantiations of similar to the following one well formed Page 67 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 68 7 Generic Specifications spec LisST LENGTH NATURAL LisT LENGTH NATURAL_ARITHMETIC end To understand this point consider the following variant of spec WRoNG LisT LENGTH sort Elem NATURAL ARITHMETIC and List Rv sort Elem then end The specification WRONG_LIST_LENGTH is fine as long as one does not need to instantiate it with as argument specifica tion The instantiation WRONG_LIST_LENGTH NATURAL_ARITHMETIC is ill formed since some symbols of the argument specification are shared with some symbols of the body and not already occurring in the parameter of the instantiated generic specification which is illegal Of course the same problem will occur with any argument specification which provides e g the sort Nat As a consequence one should remember two essential points First an instantiation is ill formed as soon as there are so
131. end Since the loose specification PARTIAL_ORDER has models where lt is in terpreted by a partial ordering relation the proof obligation corresponding to the above implies annotation cannot be discharged However since an notations have no impact on the semantics the specification IMPLIES_DOES_ Nor HOLD is not inconsistent it just constrains the interpretation of lt to be a total ordering relation Attributes may be used to abbreviate axioms for associativity commu tativity idempotency and unit properties spec MONOID sort Monoid ops 1 Monoid __ _ Monoid x Monoid Monoid assoc unit 1 end The above example introduces a constant symbol 1 of sort Monoid then a binary operation symbol which is asserted to be associative and to have 1 as unit element The assoc attribute abbreviates as expected the following axiom 2 Monoid e 2 2 The unit 1 attribute abbreviates Monoid e rx 1 2 A 1 2 2 Page 10 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 1 Loose Specifications 11 Note that to make the use of unit 1 legal it is necessary to have previously declared the constant 1 to respect the linear visibility rule Other available attributes are comm which abbreviates the obvious axiom stating that a binary operation is commutative and idem which can be used to assert the idempotency of a binary operation f ie that
132. ensure that values of Pos correspond to Page 40 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 5 2 Subsorts and Overloading 41 non zero values of Nat Several alternative ways of specifying the sort Pos will be considered later in this section spec POSITIVE then sort Pos x Nat e 0 end 5 2 Subsorts and Overloading It may be useful to redeclare previously defined operations using the new subsorts introduced spec POSITIVE ARITHMETIC then ops 1 Pos suc Nat Pos coa su Pos x Pos Pos Pos x Nat Pos Nat x Pos Pos end Since in POSITIVE we have defined Pos as a subsort of Nat all operations defined on natural numbers like suc and x see in Chap 3j 20 which is extended PT Pacha Chal p 81 are automatically inherited by Pos and can be applied to terms of sort Pos However according to their declarations these operations when applied to terms of sort Pos yield results of sort Nat To indicate that these results always correspond to values in the subsort Pos it is necessary to explicitly overload these operations by similar ones with the appropriate profiles This is the aim of the first three lines of operation declarations in the above example The last two operation declarations further overload to specify that also yields a result of sort Pos as soon as one of its arguments is a term of sort Pos It is quite im
133. entation and alphabetically at the end of the book Readers who are familiar with previous algebraic specification languages and especially those who have been following or participating in the design and development of CASL may prefer to skip lightly through Chaps 2 Chapter 3 however is mandatory since it is there that we introduce many CASL features that will be needed to understand the subsequent chapters In contrast Chaps 4 and 5 can be skipped at first reading if the reader is not so much interested in these features with the proviso though that there are some references to the examples given in these chapters from later chapters Chapters 6 and 7 present mainstream material and until one feels com fortable with all the main points and examples it is advisable to wait with proceeding to Chap 8 Chapter 9 is however quite orthogonal to the other chapters and can be read when desired Part of the introduction to CASL support tools in Chap assumes familiarity with concepts introduced in Chap Chapter is primarily for those who will want to follow up on this User Manual with a more detailed study of the language based on the Reference Manual It should be possible to use it as the basis for an interactive tutorial but this is not yet available Page VII FIRST PUBLIC DRAFT 17 Sep 2003 17 54 VIII Preface Acknowledgements Chapter was written by Till Mossakowski who also provided App bas
134. er constrain the interpretation of the predicate symbol lt by requiring it to be a total ordering relation All symbols introduced in a specification are by default exported by it and visible in its extensions This is for instance the case here for the sort Elem and the predicate symbol lt which are introduced in STRICT PARTIAL ORDER exported by it and therefore available in See Chap 6 for constructs allowing the explicit restriction of the set of symbols exported by a specification Page 7 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 3 Total Many Sorted Specifications In simple cases an operation or a predicate symbol may be declared and its intended interpretation defined at the same time spec TOTAL_ORDER_WITH_MINMAX then ops min x y Elem Elem when x lt y else y max x y Elem Elem y when min z y x else x end TOTAL ORDER WiTH MINMAX extends by introducing two binary operation symbols min and maz for which a functional notation is to be used so no place holders are given The intended interpretation of the symbol min is defined simultaneously with its declaration and the same is done for maz For instance op min z y Elem Elem when x lt y else y abbreviates op min Elem x Elem Elem Vz y Elem e min z y when x lt y else y and similarly for maz The when else construct used above is itself an abbrevia tion Indeed mi
135. ere we are unable to discharge this proof obligation A careful analysis of the proof attempt shows that the proof fails since it could be the case that simultaneously with the receipt of a repaired message for the physical unit pu we nevertheless detect again a failure of the same unit From this analysis we conclude that the following axiom in STATUS EVOLUTION is not adequate e status s pu FailureWithAck REPAIRED pu is_in msgs gt next_status s msgs OK This means we must fix the STATUS_EVOLUTION specification and replace the above axiom by e status s pu FailureWithAck REPAIRED pu is_in msgs gt next_status s msgs OK when PU OK s msgs else Failure WithoutAck Once the specification STATUS EVOLUTION is modified as explained above we can prove that the expected property holds Page 144 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 10 Designing the Architecture of the Steam Boiler Control System 145 To conclude the reader should keep in mind that the validation of the specification is a very important task that deserves some serious attention In this section we have only briefly illustrated some typical proof attempts that would naturally arise when validating the STEAM_BOILER CONTROL_SYSTEM specification and obviously many other proof attempts are required to reach a stage where we can trust our requirements specification of the steam boiler control system C 10 Designing the Archite
136. ert it follows that any value denotable by a term of the form merge can also be denoted by a term built with empty and insert and no merge Hence for the specifi cation proofs by induction on Container only need to consider empty and insert and not merge as was the case for GENERATED_CONTAINER Generated specifications need not be loose spec GENERATED_SET sort Elem generated type Set empty insert Elem Set pred _is_in__ Elem x Set ops __ e Elem Set insert e empty Set x Set Set remove Elem x Set Set Ve Elem 8 5 Set e e is in empty e e is in insert e S e V e is in S e S 5 amp Elem e is in S lt is in S 96 equal sets 96 e is in SU S e is_in S V e is in 57 e e is in remove e S e e e S then implies Ve e Elem S Set e insert e insert e insert e S e insert e insert e 5 insert e insert e S generated type Set empty Elem U Set Set _U_ Set x Set Set assoc comm idem unit empty end Although generated specifications are in general loose they need not be so as illustrated by the above GENERATED specification where the axiom equal_sets combined with the axioms defining 7 fully constrains the interpretations of the sort Set and of the constructors empty and insert once an interpretation for the sort Elem is chosen
137. ete syntax definition of CASL in SDF syntax directed ed itors within the ASF SDF Meta Environment come for free Recent devel opments in the Meta Environment allow even the development of a CASL programming environment Such an environment would include syntax directed editors for CASL and an open archictecture based on a software coor dination architecture ToolBus BK98 in order to communicate with other CASL tools such as the ELAN CASL toolset 10 6 Other tools The following tools could be added provided until early September there is a stable version available e The CASL consistency checker With the CCC one can interactively check whether a CASL specification is consistent Translation CASL to OCAML developed at Paris Poitiers Translation CASL to Haskell developed in Bremen Page 85 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 11 Foundations Donald Sannella and Andrzej Tarlecki A complete presentation of CASL is in the CASL Reference Manual This CASL User Manual has introduced the potential user to the features of CASL mainly by means of illustrative examples It has presented and dis cussed the typical ways in which the language concepts and constructs are expected to be used in the course of building system specifications Thus the presentation in Chaps 119 focused on what the constructs and concepts of CASL are for and how they should and should not be used We tried to make these points as
138. ewrite engine revised version in CoF November 2000 Till Mossakowski CASL From semantics to tools In S Graf and M Schwartzbach editors TACAS 2000 volume 1785 of Lecture Notes in Computer Science pages 93 108 Springer Verlag 2000 Till Mossakowski Relating CASL with other specification languages the institution level Theoretical Computer Science 286 367 475 2002 Peter D Mosses editor CASL Reference Manual Lecture Notes in Com puter Science Springer 2003 To appear L C Paulson Isabelle A Generic Theorem Prover Number 828 in LNCS Springer Verlag 1994 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 List of Named Specifications SIDE odd ree 6 bed 7 TM 8 digg d ahead 8 TAA dico rao eer 9 m 9 dr nad od 10 debe ed 10 11 11 Las ates 12 12 wedtam 13 14 ee 15 c 15 16 ak Sele 18 a eer ne d 18 tale Kine Sea age GA 18 19 al
139. f the form ti t2 gt t3 is often wrong if t1 and t2 may be undefined because the equality t t4 would be implied when both 1 and are undefined since then the strong equation t1 2 would hold The above specification provides a typical example of such a situation 2 gt 2 2 gt 2 would be wrong since it would entail that any two arbitrary values y 2 are equal it is enough to choose an x greater than y and z to make y z and z z both undefined Therefore to avoid such undesirable consequences of undefinedness it is advisable to use existential equations instead of strong equations in the premises of conditional equations involving partial operations An alternative is to add the relevant definedness assertions explicitly to the equations in the premises Page 35 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 5 Subsorting Subsorts and supersorts are often useful in CASL specifications Many examples naturally involve subsorts and supersorts CASL provides means for the declaration of a sort as a subsort of another one when the values of the subsort are regarded a special case of those in the other sort The aim of this chapter is to discuss and illustrate how to handle subsorts and supersorts in CASL specifications 5 1 Subsort Declarations and Definitions Subsort declarations directly express relationships between carrier sets spec GENERIC_MoNoID_1 sort Elem sorts Ele
140. f the steam boiler control system Finally in Sec C 11 we offer some concluding remarks C 2 Getting Started As explained in Sec C 12 3 in each cycle the steam boiler control system collects the messages received performs some analysis of the information contained in them and then sends messages to the physical units We will therefore start with the specification of some elementary datatypes such as received messages and sent messages To specify the messages sent and received we follow Secs C 12 5 and 12 6 Note that some messages have parameters e g pump number pump state pump controller state mode of operation and we must therefore specify the corresponding datatypes as well For the sake of clarity we group together all similar messages e g all re paired messages all failure acknowledgement messages by introducing a suitable parameter physical unit A physical unit is either a pump a pump controller the water level measuring device or the output of steam measuring device Remember that we do not specify the physical units as such since we do not specify the physical environment of the steam boiler we do not spec Page 117 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 118 C Case Study The Steam Boiler Control System ify the steam boiler either we only specify the steam boiler control system Hence the datatype physical unit is just an elementary datatype that says th
141. f the valid static limits that is between 0 and W 2 The program detects that the unit indicates a value which is incompatible with the dynamics of the system TRANSMISSION 1 The program receives a message whose presence is aberrant 2 The program does not receive a message whose presence is indispensable Page 156 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 References The bibliography style is to be numerical in the final version 02 BDH 01 BJKOOO BK98 BMVO83 BSVV02 CoF CRV03 S Autexier and T Mossakowski Integrating HOL CASL into the de velopment graph manager Maya In A Armando editor Frontiers of Combining Systems 4th International Workshop volume 2309 of Lecture Notes in Computer Science pages 2 17 Springer Verlag 2002 M G J van den Brand A van Deursen J Heering H A de Jong M de Jonge T Kuipers P Klint L Moonen P A Olivier J Scheerder J J Vinju E Visser and J Visser The ASF SDF Meta Environment a component based language development environment In R Wilhelm editor C C 01 volume 2027 of LNCS pages 365 370 Springer Verlag 2001 M G J van den Brand H A de Jong P Klint and P Olivier Efficient annotated terms Software Practice amp Experience 30 259 291 2000 J A Bergstra and Klint The discrete time ToolBus a software coordi nation architecture Science of Computer Programming 31 2 3 205 229 July 1998 M G J van
142. f z x Asserting x to be associative using the attribute assoc makes the term z y z well formed assuming x y z of the right sort while otherwise grouping parentheses would be required Moreover it is expected that some tools e g systems based on rewriting may use the assoc attribute so it is generally advisable to use this attribute instead of stating the same property by an axiom the same applies to the other attributes Genericity of specifications can be made explicit using parameters spec GENERIC MoNoID sort Elem sort Monoid ops inj Elem Monoid 1 Monoid Monoid x Monoid Monoid assoc unit 1 Elem e inj z inj y y The above example describes monoids built over arbitrary elements of sort Elem The intention here is to reuse the specification GENERIC MONOID to derive from it specifications of monoids built over say characters symbols etc In such cases it is appropriate to emphasize the intended genericity of the specification by making explicit in a distinguished parameter part here sort Elem the piece of specification that is intended to vary in the derived spec ifications In these it will then be possible to instantiate the parameter part as desired in order to specialize the specification as appropriate to obtain e g a specification of monoids built over characters A named specification with one or more parameter s is called gener
143. gnature of N ATURAL must be equal to N This property reflects the fact that a software module is supposed to use what it is given exactly as supplied without altering it Similarly the line Cont_DEL DEL NATURAL given declares a E RTT whic di the component C expands it into a model of The final result i is A i D More complex examples of result expressions will be illustrated in examples below As in the rest of CASL visibility is linear in architectural specifications meaning that any component must be declared before being used e g the component N should be declared before being referred to by given N in the declaration of the component C in the architectural specification Component names such as and D in are local to the ar chitectural specification where they are declared and are not visible outside it S There can be several distinct architectural choices for the same quirements specification For instance the following architectural specification corresponds to a dif ferent architectural choice for implementing our REQ specification arch spec SYSTEM 1 units N Conr Der Narman given result CD The architectural specifications SYSTEM and SYSTEM _1 both provide mod els of REQ However the former insists on an implementation made of three components while the latter insists on an implementation made of two com ponents
144. he combined use of specifications taken from different libraries see Part VI for further details Page 223 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 224 9 Libraries Validated libraries can be located via the web pages and to be mirrored at several sites to ensure their accessibility It is likely that new versions of existing libraries will be produced e g providing further operations whose usefulness was not realized beforehand Although the assignment and use of library version numbers allows users to protect their specifications from changes due to new versions see Sec 9 3 at least the names used in an installed library should not change much between versions Libraries should include appropriate annotations In particular parsing and display annotations can be provided The above example illustrates a further kind of annotation used to provide literal syntax for numbers in CASL The effect of the annotation is that when using the appropriate specifications from the library BASIC NUMBERS conventional decimal notation can be used for integers and decimal fractions e g 42 2 718 10E 12 Libraries can include items downloaded from other libraries library BAsIC STRUCTUREDDATATYPES from Basic NUMBERS get NAT INT spec LisT sort Elem given NAT spec ARRAY given INT Individual specifications and other items can be downloaded from other li braries For example as
145. he component PR an implementation of the predicted state variables for the next cycle the compo nent ME provides an implementation of next mode and of next_nbSTOP and the component MTS provides an implementation of messages_to_send The specifications of the components ME and MTS are simple enough to be directly implemented The specifications of the components FD and PR can be refined as follows arch spec ARCH_FAILURE_DETECTION FO FARE PUMP FAILURE PUMP_CONTROLI Pump_CONTROLLER_FAILURE EVEL LEVEL FAILURE gt STEAM FAILURE result AS SBCS_STATE e 5 5 PF S PCF S SF S LF S hide Pump Controller OK Steam_OK Level OK end The above architectural specification ARCH FAILURE DETECTION refines the specification SBCS STATE FAILURE_DETECTION of the component FD in ARCH ANALYSIS and introduces a component for each kind of failure de tection Then the component PU implements PU and in the result unit expression we hide the auxiliary predicates provided by the components PF PCF SF and These auxiliary predicates are already hidden the specification However remember that in the specification of a generic component the target specification is always an implicit extension of the argument specifica tions This is why it is needed to hide the auxiliary predicates at the level of the result unit expression Page 147 FIRST PUBLIC DRAFT 17 Sep 20
146. he illustrative alternative specifications Page 219 FIRST PUBLIC DRAFT 17 8 2003 17 54 220 9 Libraries given in any order e g PARTIAL ORDER above could be given after TOTAL ORDER Mutual recursion between specifications is prohibited When two specifi cations each make use of symbols declared in the other the declarations of those symbols have to be duplicated or moved to a preceding specification that can then be referenced by them both All kinds of named specifications can be included in libraries library USERMANUAL EXAMPLES STRICT_PARTIAL_ORDER Spec GENERIC MoNorD sort Elem ge INTEGER AS TOTAL ORDER vies Lisr As MoNOID sort Elem arch spec SYSTEM unit spec CoNT COMP Items in libraries can be any kind of named specification as illustrated above simple named specifications generic specifications named view defini tions generic view definitions and architectural and unit specifications We shall henceforth refer to them generally as library items Libraries themselves never include anonymous specifications such as dec larations of sorts and operations Moreover the symbols declared by a library item are not automatically available for use in subsequent items an explicit reference to the name of the library item is required to import the item Technically each library item is said to be closed being interpreted without any p
147. he underlying institution but just reflects the way in which the structuring and architectural constructs are defined for an arbitrary institution Page 90 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 11 Foundations 91 A formal refinement concept for CASL specifications is introduced As a basis for the CASL methodology of systematic development of software systems in Part V of the Reference Manual we provide a formal concept of a correct refinement step leading from one CASL specification to another presumably more detailed and closer to the final realization of the system under development The proof systems mentioned above may be applied here for proving correctness of such development steps The foundations of our CASL are rock solid All this work on the mathematical underpinnings of CASL and related specification and development methodology as documented in the Reference Manual should make it exceptionally trustworthy at least in the sense that it provides a formal point of reference against which all the claims may and should be checked Page 91 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 Appendices A CASL Quick Reference CASL consists of several major parts which are quite independent and may be understood and used separately Basic specifications Denote classes of partial first order structures algebras where the func tions are partial or total and where also predicates
148. here we assume that the predicted values will take care of the static limits 0 and W for the steam 0 and C for the water level thus we do not need to check these static limits explicitly here Page 133 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 134 C Case Study The Steam Boiler Control System spec STEAM_FAILURE then pred Steam_OK State x FinSet R_Message Vs State msgs FinSet Rt Message e Steam OK s msgs lt Vu Value e STEAM v msgs gt low steam_predicted s v v high steam_predicted s end spec LEVEL FAILURE SBCS STATE 5 then pred Level OK State x FinSet R Message Vs State msgs FinSet R Message e Level OK s msgs lt Vu Value e LEVEL v e msgs gt low level_predicted s lt v v high level_predicted s end C 5 6 Summing Up We now have all the ingredients necessary for the specification of the predi cate PU OK This is done in the FAILURE DETECTION specification which integrates together all the specifications related to failure detection spec FAILURE DETECTION and PUMP FAILURE and PUMP CONTROLLER FAILURE and STEAM FAILURE and LEVEL FAILURE then pred PU State x FinSet R Message x PhysicalUnit Vs State msgs FinSet R Message pn PumpNumber e PU OK s msgs Pump pn lt gt Pump OK s msgs pn e PU OK s msgs PumpController pn gt Pump Controller OK s msgs pn e PU OK s msgs OutputOfSteam
149. hese predictions are only meaningful as long as no failure of the message transmission system has been detected but if this is not the case the steam boiler control system switches to the EmergencyStop mode and stops so no predictions are needed anyway The corresponding specifications are described in the next subsections Page 135 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 136 C Case Study The Steam Boiler Control System C 6 1 Predicting the Output of Steam and the Water Level To predict the intervals in which the output of steam and the water level are expected to stay during the next cycle we will proceed as follows 1 Following the analysis sketched above when we are in the state s and have received the messages msgs to predict the interval in which the out put of steam is expected to stay during the next cycle we first should compute the adjusted_steam interval this interval is either the inter val reduced to the received_steam value if we can rely on it ie if PU OK s msgs OutputOfSteam holds or the steam_predicted interval stored in the state s at the previous cycle 2 Then we use the maximum gradients of increase and decrease i e U1 and U2 to predict the interval in which the output of steam is expected to stay during the next cycle For this we use two auxiliary operations low predicted steam and high predicted steam to compute the lower and upper bounds of this interval 3 We proceed simil
150. ic The body of the generic specification is an extension of what is specified in the parameter part Hence an alternative to the above generic specification is the following less elegant non generic specification which cannot be specialized by instantiation spec NON_GENERIC_MONOID sort Elem then sort Monoid ops inj Elem Monoid 1 Monoid Monoid x Monoid Monoid assoc unit 1 Vz y Elem e inj z inj y y end Page 11 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 12 3 Total Many Sorted Specifications A generic specification may have more than one parameter and parame ters can be arbitrary specifications named or not When reused by reference to its name a generic specification must be instantiated Generic specifications and how to instantiate them are discussed in detail later in Chap 7 Using generic specifications when appropriate improves the reusability of specifica tion definitions References to generic specifications always instantiate the parameters spec GENERIC COMMUTATIVE MONOID sort Elem sort Elem then Vz y Monoid e end The above generic e Mer eie dn tfo is de fined as an extension of which should therefore be instan tiated as explained above Instantiating a generic specification is done by pro viding an argument specification that fits the parameter part of the generic specification to be instantiated It is however qu
151. ically deduced taking into account the explicitly specified fitting symbol map if any the situation here is quite similar to a renaming where a signature morphism is deduced from a symbol map The instantiation is defined if all models of the argument specification when reduced along the induced fitting signature morphism provide models of the parameter part In particular the symbols provided by the argument specification must have the properties if any specified in the parameter for their counterparts When this is the case we get not only a signature morphism but also a fitting specification morphism from the argument specification to the parameter specification In the above example since the parameter of MoNorD is trivial it is obvious that the instantiation is defined The effect of the instantiation is to make the union of the argument spec ification and of the non generic equivalent of the generic specification re named according to the induced fitting signature morphism In particular a side effect of the instantiation is to rename the symbols of the generic specifica tion according to the fitting signature morphism induced by the instantiation In our WORD example the operation symbol inj Elem Monoid is renamed into inj Nat Monoid while the operation symbols 17 and x are left unchanged as well as the sort Monoid Thus the specification WoRD abbreviates the following specification
152. illed even if there is no syntactic correspondence between the axioms given in and those in As may be clear by now the exact rules for when the fitting between pa rameter and argument symbols can be left implicit are quite sophisticated It seems best to make the intended fitting explicit whenever it is not completely obvious using the notation for fitting arguments illustrated in the following examples The intended fitting of the parameter symbols to the argument symbols may have to be specified explicitly spec NAT_WoRD_2 GENERIC MONOID NATURAL SUBSORTS fit Elem gt Nat end The correspondence between the symbols required by the parameter and those provided by the argument specification can be made explicit using so called fitting symbol maps For instance the above NAT WORD 2 specifica tion which differs from NAT WOoRD only regarding the presence of subsorts of Nat is obtained as an instantiation of fitting the param eter part sort Elem to the NATURAL SUBSORTS specification The mapping Page 60 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 7 1 Parameters and Instantiation 61 between the parameter sort Elem and the sort Nat provided by SuBsoRrTS is described by the fitting symbol map fit Elem Nat A generic specification may have more than one parameter spec Pair sort Elem1 sort Elem2 Using several parameters is merely a notational convenience since they ar
153. imported from an extended specification as it is the case here for x Of course it does not apply between named specifications i e Page 12 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 1 Loose Specifications 13 the same symbol may be used in different named specifications with entirely different interpretations Note that for operation and predicate symbols the same name same thing principle is a little more subtle than for sorts the name of an operation or of a predicate includes its profile of argument and result sorts so two operations defined with the same symbol but with different profiles do not have the same name the symbol is just overloaded When an overloaded symbol is used the intended profile is to be determined by the context e g the sorts of the arguments to which the symbol is applied Explicit disambiguation can be used when needed by specifying the profile or result sort in an application Note that overloaded constants are allowed in CASL e g empty may be declared to be a constant of various sorts of collections Datatype declarations may be used to abbreviate declarations of sorts and constructors spec CONTAINER sort Elem type Container empty insert Elem Container pred _is_in__ Elem x Container Ve e Elem Container e e is n empty e e is in insert e C amp e e V e is in C end Specifications of datatypes with
154. in a b c not even if _ __ were to be included in the same left associativity annotation When an operation symbol is declared with the associativity attribute assoc a left associativity annotation for that symbol is provided automati cally Thus in practice explicit associativity annotations are needed only for non associative operations such as subtraction and division Libraries and library items can have author and date annotations library USERMANUAL EXAMPLES authors Michel Bidoit lt bidoit lsv ens cachan fr gt Peter D Mosses lt pdmosses brics dk gt dates 15 Oct 2003 1 Apr 2000 spec STRICT_PARTIAL_ORDER Yoauthors Michel Bidoit ena arian 5 dates 10 July 2003 spec INTEGER_ARITHMETIC_ORDER An author annotation at the beginning of a library indicates the collec tive authorship of the entire library one preceding an individual library item indicates its specific authorship A date annotation at the beginning of a library should indicate the release date of the current version of the library It may also give the release dates of previous major versions including that of the original version A date anno tation on an individual library item should indicate when that item was last changed and optionally the dates of previous changes Page 222 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 9 2 Distributed Libraries 223 9 2 Distributed Libraries Libraries can
155. in this chapter A constant may also be declared to be partial allowing its value to be undefined in some models Variables however range only over defined values Terms containing partial functions may be undefined i e they not denote any value For instance the value of the term choose empty may be undefined Functions even total ones propagate undefinedness If the term choose S is undefined for some value of 5 then the term insert choose S S is undefined as well for this value of S although insert is a total function Predicates do not hold on undefined arguments CASL is based on classical two valued logic A predicate symbol is inter preted by a relation and when the value of some argument term is undefined the application of a predicate to this term does not hold For instance if the term 8 is undefined then the atomic formula choose is_in S does not hold Equations hold when both terms are undefined In CASL equations are by default strong which means that they hold not only when both sides denote equal values but also when both sides are simultaneously undefined For instance let us consider the equation insert choose S insert choose S empty insert choose S empty Either choose S is defined and then both sides are defined and denote equal values due to the axioms on insert or choose S is undefined and then both sides are un
156. inition op 8 partial constant definition ops multiple declarations definitions A 1 1 4 Predicate Declarations and Definitions pred 51 9696 predicate declaration pred p constant predicate declaration preds 1 9696 predicates declaration pred p vl s1 un sn 9696 predicate definition pred F 9696 constant predicate definition pred p vil vim si 9696 abbreviated arguments preds 9696 multiple declarations definitions A 1 1 5 Datatype Declarations type 9696 datatype declaration with alternatives types s 1 9696 multi sorted datatype declaration sn An generated types 9696 generated datatype declaration free types 9696 free datatype declaration Alternatives A f s1 5 sk total constructor function f s1 sk partial constructor function total constructor and selector functions fC fi 2st total constructor partial selector functions f ftl fim si 9696 abbreviated selectors constant constructor value sort 8 subsort sorts s1 8k subsorts 1 Am multiple alternatives A 1 1 6 Sort Generation Constraint generated sorts generated sorts Ops 9696 generating operations preds types 9696 generated sorts and generating constructors Page 97 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 98 A CASL Quick Reference
157. ioms lists of axioms A 1 1 Declarations and Definitions A 1 1 1 Sort Declarations and Definitions sort s sorts 81 5 sorts s s 9696 sorts 1 5n lt s sorts s lt 81 s lt sn sorts 51 sn sort 0 5 F 1 1 2 Function Declarations op op op op op O O O 000 0 Page 96 5 5 FIRST PUBLIC DRAFT sort declaration sorts declaration subsort declaration subsorts and supersort declaration subsort and supersorts declaration isomorphic sorts declaration subsort definition and Definitions f slxX xsn 8 total function declaration f sl x xsn 5s partial function declaration fis 8 8 880 90 associative binary function f sxs s comm 9696 commutative binary function f sxs s idem 9696 idempotent binary function f sxs s unit T 9696 unit term for binary function 8 8 55 multiple function attributes Tf yfniws functions declaration f v1 51 vn sn s T total function definition f v1 s1 vn sn s T 9696 partial function definition f vutl vim si abbreviated arguments multiple declarations definitions 17 Sep 2003 17 54 A 1 Basic Specifications 97 A 1 1 3 Constant Declarations and Definitions op c s constant declaration op c s partial constant declaration 1 s constants declaration op c s T 9696 constant def
158. ion are the most used specification building operations In contrast with extension whose purpose is to extend a given piece of specification by new symbols and axioms union is generally used to combine two self contained specifications Union of specifications is obviously an associative and commutative operation All symbols introduced by a specification are by default exported by it and visible in its extensions or in its unions with other specifications Vari ables are not considered as symbols and never exported Remember also the same name same thing principle in the above 118 5 specification it is therefore the same sort Elem which is used to construct both lists and sets Arbitrary parts of specifications can have initial semantics spec LIST_CHOOSE sort Elem sort Elem and SET PARTIAL CHOOSE 2 sort Elem then ops elements of List Set choose List Elem Ve Elem L List elements_of empty empty elements of cons e L e U elements of L def choose L 1 empty choose L choose elements_of L end spec SET_TO_LIST sort Elem sort Elem then op list_of__ Set List VS Set elements of list of S S end The specification is built as an extension of the union of and see Chap 4 p 130 This extension introduces an operation elements_of as in LIST_SET and a partial operation choose which are defined by some axioms In lists are defined by a
159. ion system and due to the fact that transmission time can be neglected the steam boiler control system must in principle receive only one repaired message for a given failure Note that this is not contradictory with the until part of the sen tences describing the repaired messages in the informal requirements cf Sec 126 To summarize we consider we receive an unexpected message when e the program receives initialization messages but is no longer in initializa tion mode or e the program receives for some physical unit a failure acknowledgement without having previously sent the corresponding failure detection mes sage or receives redundant failure acknowledgements or e the program receives for some physical unit a repaired message but the unit is OK or its failure is not yet acknowledged We now have all the ingredients required to specify the Transmission OK predicate taking into account both static and dynamic aspects which leads to the following MESSAGE T RANSMISSION SYSTEM FAILURE specification 5 We must confess that this belief is induced by our intuition about the behaviour of the system Indeed nothing in the requirements allows us to make either this interpretation or the opposite one Although not essential this assumption will simplify the axiomatization Page 130 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 5 Specifying the Detection of Equipment Failures 131 spec MESSAGE
160. is means that the specification SBCS STATE will be subject to iterated extensions where we introduce the new observers that are needed For instance in Sec 126 it is explained that when the STOP mes sage has been received three times in a row the program must go into the EmergencyStop mode We need therefore an observer 1 a state variable to record the number of times we have successively received the STOP message So in the sequel we will start from the following specification of states spec SBCS STATE 1 then sort State ops mode State Mode nbSTOP State Nat end Introducing the new observer nbS TOP means that we will have to specify a corresponding nezt nbS TOP operation in the SBCS_ANALYSIS specification Page 122 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 4 Specifying the Mode of Operation 123 C 4 Specifying the Mode of Operation Our next step is the specification of the various operating modes in which the steam boiler control system operates As explained in Sec we do not take into account the Initialization mode in this specification According to Sec 1214 the operating mode of the steam boiler control system depends on which failures have been detected see e g all physical units are operating correctly a failure of the water level measuring unit detection of an erroneous transmission It depends also on the expected evolution of the water level see If the water le
161. ite frequent that the instantiation is trivial i e the ar gument specification is identical to the parameter one This is the case for the above example where the generic specification GENERIC MONOID is instanti ated by providing the same argument specification sort Elem as the original parameter spec GENERIC COMMUTATIVE MONOID 1 sort Elem sort Blem then op Monoid x Monoid Monoid comm end is an alternative version of the for mer specification where instead of requiring explicitly with an axiom the commutativity of the operation x we require it using the attribute comm As explained before it is in general better to describe such requirements using attributes rather than explicit axioms since it is expected that some tools will rely on these attributes for specialized algorithms e g ACI unification This example illustrates also an important feature of CASL the same name same thing principle The operation symbol x is indeed declared twice with the same profile first in and then again in GENERIC COMMUTATIVE MONOID 1 the second declaration being enriched by the attribute comm This is perfectly fine and defines only one binary operation symbol with the corresponding arity according to the same name same thing principle This principle applies to sorts as well as to operation and predicate symbols It applies both to symbols defined locally and to symbols
162. ive specifications are both extended perhaps indirectly in the same specification the principle does apply and inconsistency might then arise Thus in general it is advisable for the developers of a library to respect the same name same thing principle when choosing symbols throughout the library In any case this is obviously helpful to those who might later browse the library Alternative specifications for the same symbols should therefore be given in separate libraries Specifications can refer to previous items in the same library library USERMANUAL EXAMPLES spec STRICT_PARTIAL_ORDER spec TOTAL ORDER STRICT PARTIAL ORDER then spec PARTIAL ORDER STRICT PARTIAL ORDER then Although we may often regard libraries as sets of named specifications they are actually sequences and the order in which the specifications occur is significant Specification names have linear visibility each specification can refer only to the names of the specifications that precede it Thus a series of extensions has to be presented in a bottom up fashion starting with a specification that is entirely self contained containing no references to other specifications at all Each specification name in a library has a unique defining occurrence so overriding cannot arise Extensions that do not refer to each other may be 1 If we intended our comprehensive USERMANUAL EXAMPLES library for general use we would remove all t
163. ledgement message has been sent by the program and received by the physical units PUMP CONTROL REPAIRED n This message indicates that the cor responding control unit has been repaired It is sent by the physical units until a corresponding acknowledgement message has been sent by the pro gram and received by the physical units LEVEL REPAIRED This message indicates that the water level measur ing unit has been repaired It is sent by the physical units until a cor responding acknowledgement message has been sent by the program and received by the physical units STEAM REPAIRED This message indicates that the unit which mea sures the outcome of steam has been repaired It is sent by the physical units until a corresponding acknowledgement message has been sent by the program and received by the physical units PUMP FAILURE ACKNOWLEDGEMENT n this message the phys ical units acknowledge the receipt of the corresponding failure detection message which has been emitted previously by the program PUMP CONTROL FAILURE ACKNOWLEDGEMENT n By this mes sage the physical units acknowledge the receipt of the corresponding failure detection message which has been emitted previously by the program Page 155 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 156 C Case Study The Steam Boiler Control System LEVEL FAILURE ACKNOWLEDGEMENT By this message the phys ical units acknowledge the receipt of the corresponding failure detection
164. llowing version of spec My_SyMBOL_TABLE sort Symbol sort Symbol NXTURAL ARITHMETIG where we still have a parameter for symbols but decide that the attributes are natural numbers end Page 62 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 7 2 Compound Symbols 63 Composition of generic specifications is expressed using instantiation spec SET LisT sort Elem LisT SELECTORS sort Elem fit Elem gt List end The above generic specification SET or 8 describes sets of lists of ar bitrary elements and is obtained by an instantiation of the generic specifi cation whose parameter sort Elem is instantiated by the specification itself trivially instantiated Since the trivially instantiated specification exports two sorts Elem and List it is of course necessary to specify in the instantiation of the fitting map from the parameter sort Elem to the argument sort List Note that the following specification spec MISTAKE sort Elem GENERATED SET LIST SELECTORS sort Elem just provides sets of arbitrary elements and lists of arbitrary elements since the absence of explicit symbol map entails that the generic specification GEN IERATED SET is instantiated by the identity fitting map Elem gt Elem 1f this was indeed the desired effect one should rather write instead spec SET AND LIST sort Elem GENERATED SET sort Elem and sort Elem end As illustrated by
165. lustrative examples For instance let us consider the specification of next_mode in it is advisable to prove that all the cases considered in the spec ification of nert mode are mutually exclusive and that their disjunction is equivalent to true This is a typical example of internal validation of the specification since we just consider the text of the specification to decide which proof attempt will be performed without considering the informal re quirements again We do not spell out the corresponding proofs here but the reader can easily check that indeed the operation next mode is well defined i e all cases are mutually exclusive and their disjunction is equivalent to true In the same spirit we can prove that the same pump cannot be simul taneously be ordered to activate and to stop that we never resignal a failure which has already been signaled that as long as the operating mode is not set to EmergencyStop the water level is safe etc Let us now consider an example of external validation According to our understanding of failure detection see Sec 5 if we have detected a failure of some physical unit pu so PU_OK does not hold for pu then the status of this physical unit should not be set to OK The corresponding proof obligation reads as follows Vs State msgs FinSet R_Message pu PhysicalUnit e Transmission OK s msgs PU s msgs pu gt 7 nezt_status s msgs pu OK However h
166. ly the same effect as the so called nega tion by default or closed world assumption principles in logic programming More generally it is often convenient to define a predicate within a freeness constraint since by doing so one has to specify the positive cases only Page 19 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 20 3 Total Many Sorted Specifications Operations may be safely defined by induction on the constructors of a free datatype declaration spec NATURAL_ARITHMETIC then ops 1 Nat suc 0 Nat x Nat Nat assoc comm unit 0 Nat x Nat Nat assoc comm unit 1 y Nat e x suc z y 0 0 e suc y z x y end To define some operation on a free datatype it is generally recommended to make a case distinction with respect to the various constructors defined This is illustrated by the above definitions of and x although for the operation the case for the constructor 0 is already taken care of by the attribute unit op More care may be needed when defining operations om free datatypes with axioms relating the constructors spec INTEGER_ARITHMETIC then ops 1 Int suc 0 b o Int x Int Int assoc comm unit 0 i Int x Int Int _ Int x Int Int assoc comm unit 1 Int e z suc y suc z y e x pre y pre z y e suc y
167. m lt Monoid ops 1 Monoid Monoid x Monoid Monoid assoc unit 1 end The above example declares the sort Elem to be a subsort of Monoid or symmetrically the sort Monoid to be a supersort of Elem Hence the spec ification GENERIC MONOID 1 is quite similar to the specification given in Chap 3 p 11 the only difference being the use of a subsort ing relation between Elem and Monoid instead of an explicit inj operation to embed values of sort Elem into values of sort Monoid In contrast to most other algebraic specification languages providing sub sorting facilities subsorts in CASL are interpreted by arbitrary embeddings 38 5 Subsorting between the corresponding carrier sets In the above example the subsort declaration Elem lt Monoid induces an implicit unnamed embedding from the carrier of the sort Elem into the carrier of the sort Monoid Thus the main difference between and GENERIC_MONOID_llis that the embedding is explicit and named inj in while it is implicit in GENERIC 1 Note that interpreting subsorting relations by embeddings rather than inclusions does not exclude models where the carrier of the subsort hap pens to be a subset of the carrier of the supersort and the embedding a proper inclusion Embeddings are just slightly more general than inclusions and technically not much more complex Operations declared on some sort are automatically inherite
168. map is applied to the component Elem also where it occurs in List Elem providing a sort List Nat Thus compound sorts can be seen as a convenient way of implicitly completing the instantiation by an appropriate renaming of the compound sorts introduced by the generic specification spec Two LisrTs NATURAL Provides the sort List Nat and INTEGER 9696 Provides the sort List Int end Using a compound sort List Elem proves particularly useful in the above example T wo LisTS where we make the union of two distinct instantiations of have used an ordinary sort List then an uninten tional name clash would have arisen and we would have to complete each instantiation by an explicit renaming of the sort List Note that in the specification we have two sorts List Nat and List Int hence two overloaded constants empty one of each sort which may need disambiguation when used in terms How to disambiguate terms is explained in Chap 3 p 13 Similarly we have overloaded operation symbols cons head tail and reverse but in general their context of use in terms will be enough to disambiguate which one is meant spec Two LisTrS 1 INTEGER ARITHMETIC T fit Elem gt Nat and INTEGER Anrr METIC 1 fit Elem Int end And the specification TWO LISTS would have been inconsistent due to the same name same thing principle and the fact that List is defined by a free type con struct Pag
169. me expected values according to the history of the system i e according to the dynamics of the system and to the messages previously sent by the steam boiler control system In particular the detection of failures of the physical units relies on the fact that we have effectively received the necessary messages If we have not received these messages then we should conclude there has been a failure of the message transmission system see below and in these cases see the specification the steam boiler control system switches to the EmergencyStop mode The further detection of failures of the physical units in addition to the already detected failure of the message transmission system is therefore irrelevant in such cases Let us now consider the message transmission system The part of Sec C 12 7 devoted to the description of potential failures of the message transmission system is quite short Basically it tells us that we should check that the steam boiler control system has received all the messages it was expecting and that none of the messages received is aberrant However it is important to note that the involved analysis of the received messages combines two aspects on the one hand there is some static analysis of the received messages in or der to check that all messages that must be present in each transmission are effectively present see Sec 6 These messages are exactly the messages required to proceed to the detec
170. me shared symbols between the argument specification and the body of the generic specification There fore when designing a generic specification it is generally advisable to turn auxiliary required specifications such as for LENGTH into given fixed parts 7 4 Views Views are named fitting maps and can be defined along with specifi cations view INTEGER_AS_TOTAL_ORDER TOTAL_ORDER to INTEGER ARITHMETIC_ORDER Elem Int lt gt lt end view INTEGER_AS_REVERSE_TOTAL_ORDER TOTAL ORDER to INTEGER_ARITHMETIC_ORDER Elem Int lt gt gt end spec LisrT REV WITH TWO ORDERS 1 Ms 010550 INTEGER AS TOTAL ORDER TOTAL INTEGER AS TOTAL ORDER then Post Rev ORDER VL List Int e order lt _ L reverse order __ gt _ end Page 68 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 7 4 Views 69 A view is nothing but a convenient way to name a specification morphism induced by a symbol map from a parameter specification to an argu ment specification This proves particularly useful when the same instantia tion with the same fitting symbol map is intended to be used several times naming it once for all makes its reuse easier Once a view is defined as e g above it can be referenced in instantiations as in view makes it clear that the argument is not merely a named specification with an implicit fitting map which would be written differen
171. med from words and or sequences of signs separated by double underscores indicating the positions of the arguments with any brackets balanced Page 99 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 100 A CASL Quick Reference Push onto_ Invisible mixfix identifiers such as ____ with two or more arguments are allowed Subsort embeddings give the effect of invisible unary functions A sort operation or predicate identifier can be compound with a list of identifiers appended to its final token Literal Strings and Numbers this is a string 42 3 14159 1E 9 27 3 6 Library Identifiers Names of libraries are either paths e g Basic NUMBERS _ BASIC ALGEBRA II or URLs formed from 2 70 9 Q amp V and hexadecimal codes and prefixed by HTTP FTP or FILE Version numbers of libraries are hierarchical 0 0 999 1 0 2 A 1 4 Comments This is a comment at the end of a line 4 This is an in line comment This a comment that might take several lines 96 This is for commenting out text including other kinds of comment A 1 5 Annotations A label is of the form text An end of line annotation is of the general form 96word s with a space following the word s A possibly multi line annotation is of the general form 96word with no space preceding the Page 100 FIRST PUBLIC DRAFT 17 8ep 2003
172. much water is poured into the steam boiler by the pumps which are open The information provided by the water level prediction is obviously crucial to decide whether we should activate or stop some pumps On the other hand to predict the pump state and pump controller state messages to be received at the next cycle we must know which pumps have been ordered to be activated or to be stopped From this first analysis we draw the following conclusions on how to specify the needed predictions 1 In a first step we should predict the interval in which the output of steam is expected to stay during the next cycle this prediction relies only on the just received value STEAM v if we trust it or on the previously pre dicted values for the steam production This is because the production of steam is expected to vary according to its maximum gradients of increase and decrease and nothing else 2 In the next step we should decide whether some pumps have to be ordered to activate or to stop This decision plus the knowledge about the current state of the pumps as much as we trust it and the predicted evolution of the steam production should allow us to predict the evolution of the water level 3 Then on the basis of the current states of the pumps and pump controllers together with the above made choice of pumps to be activated or stopped we can predict the states of the pumps and of the pump controllers at the next cycle Of course all t
173. n once an interpretation for the part which is extended has been chosen Page 24 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 3 Free Specifications 25 Operations can be defined by axioms involving observer operations instead of inductively on constructors spec SET_UNION_1 sort Elem sort Elem then def ops _U_ Set x Set Set assoc comm idem unit empty remove Elem x Set Set Ve Elem 8 5 Set e e is in S U S e is in S V e is in S e e is in remove e S e e is_in S end The specification is an alternative to UNION and de fines exactly the same model class While an inductive definition style was cho sen for the operations U and remove in SET UNION in UNION 1 these operations are defined implicitly by characterizing their results through the observer is in Note that this observer style does not prevent us providing a unique definition of both operations as claimed by the def annotation Similarly to the discussion on the respective merits of and of the choice between an inductive definition style and an ob server definition style is partly a matter of taste One may argue that the observer definition style is more abstract in the sense that there is no hint to any algorithmic computation of the so defined operations while the induc tive definition style mimics a recursive definition in a functional progr
174. n with illustrative ex amples and advice on the use of the different specification styles Partial functions arise naturally Chapter 4 explains how CASL supports specification of partial functions drawing attention to where special care is needed compared to specifications involving only total functions Subsorts and supersorts are often useful in CASL specifications Chapter 5 illustrates how they can be declared and defined and that they can sometimes avoid the need for partial functions The examples given so far make use of named and structured specifica tions in a simple and natural way Chapter 6 takes a much closer look at the constructs CASL provides for structuring specifications explaining how large and complex specifications are easily built out of simpler ones by means of a small number of specification building operations Chapter 7 shows how making a specification generic when appropriate improves its reusability It also introduces the constructs for expressing so called views between specifications and explains their relationship to proof obligations While specification building operations are useful to structure the text of large specifications architectural specifications are meant for imposing struc ture on models Chapter 8 will discuss and illustrate the role of architectural specifications and show how to express them in CASL Chapter 9 will explain and illustrate how libraries of named specifications ca
175. n FINSET is imported from the library BASIC STRUCTUREDDATATYPES This leads to the following PRELIMINARY specification from Basic STRUCTUREDDATATYPES get FINSET spec PRELIMINARY C 3 Carrying On As emphasized in Sec 3 the steam boiler control system is a typical ex ample of a control command system The specification of such systems always follows the same pattern e A preliminary set of specifications group all the basic information about the system to be controlled such as the specification of the various mes sages to be exchanged between the system and its environment and the specification of the various constants related to the system of interest This is indeed the aim of the specification introduced in the previous section e Then the various states of the control system should be described At this stage however it would be much too early to determine which state vari ables are needed Thus states will be represented by values of a loosely specified sort State equipped with some observers corresponding to ac cess to state variables During the requirements analysis and formalization phase we may need further observers to be introduced on a by need basis e Then a group of specification s will take care of the analysis of the received messages here of failure detection in particular On the basis of Page 120 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 3 Carrying On 121 this analysis som
176. n be formed and made available over the Internet to encourage widespread reuse and evolution of specifications Version control is of crucial importance here Page VI FIRST PUBLIC DRAFT 17 8ep 2003 17 54 Preface VII Tool support is vital for efficient use of formal specifications in connection with practical software design and development Chapter 10 presents the main tools that have been implemented so far several of them allow use of CASL specifications in connection with tools that were originally developed for other specification languages showing how CASL provides tool interoperability Chapter gives a detailed overview of the foundations of CASL which are established in the accompanying CASL Reference Manual Mos03 This User Manual is completed by three appendices App A provides an compact overview of all CASL constructs for quick reference App B intro duces a few of the many specifications that are available in the CASL libraries of basic datatypes at Bremen and finally App C will give a realistic case study of the use of CASL in practice in connection with the design of software for a Steam Boiler Organization All the main points are highlighted like this The material in the User Manual is organized in a tutorial fashion Each point is usually accompanied by an illustrative example of a complete CASL specification the names of these specifications are listed both in order of pres
177. n general loose spec GENERATED_CONTAINER_MERGE sort Elem Generate Contatven sort Elem then op Container x Container Container Ve Elem C C Container e e is in C merge C lt e is_in C V e is_in C end A generated specification is in general loose For instance CONTAINER loose since although all values of sort Container are specified to be generated by empty and insert the behaviour of the insert constructor is still loosely specified nothing is said about the case where an element is inserted to a container which already contains this element Hence ATED CONTAINER admits several non isomorphic models Page 15 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 16 3 Total Many Sorted Specifications IGENERATED CONTAINER MERGE is as loose as GENERATED_CONTAINER in what concerns insert and in addition the newly introduced operation symbol merge is also loosely specified nothing is said about what happens when merging two containers which share some elements It is important to understand that looseness of a specification is not a prob lem but on the contrary avoids unnecessary overspecification In particular loose specifications are in general well suited to capture requirements The fact that merge is loosely specified does not mean that it can pro duce new values of the sort Container On the contrary since this sort has been specified as being generated by empty and ins
178. n z y when x lt y else y abbreviates x lt y gt min z y z lt y min z y y In CASL specifications visibility is linear i e any symbol must be declared before being used In the above example min should be declared before being used to define maz Linear visibility does not imply however that a fixed scheme is to be used when writing specifications the specifier is free to present the required declarations and axioms in any order as long as the linear visibility rule is re spected For instance one may prefer to declare first all sorts and all operation or predicate symbols needed and then specify their properties by the relevant axioms Or in contrast one may prefer to have each operation or predicate symbol declaration immediately followed by the axioms constraining its inter pretations Both styles are equally fine and can even be mixed if desired This flexibility is illustrated in the following variant of the TOTAL ORDER WrTH MiNMax specification where for explanatory purposes we refrain from using the useful abbreviations explained above spec VARIANT OF TOTAL ORDER WITH MINMAX then vars Elem op min Elem x Elem Elem lt min z y e 1 lt y gt min z y y Page 8 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 3 1 Loose Specifications 9 op maz Elem x Elem Elem e lt 2 e lt y gt max z y c end Note that
179. nal discussions on the details of the constructs under con sideration and provided guidelines for many choices in the design of CASL Indeed the concrete syntax of CASL was designed only after the semantics was settled Proof systems for various layers of CASL are provided The semantics is also a necessary prerequisite for the development of mech anisms for formal reasoning about CASL specifications This is dealt with in Part IV of the Reference Manual where proof calculi that support reason ing about the various layers of CASL are presented The starting point is a formal system of deduction rules which determines a proof theoretic counter part of the consequence relation between sets of formulae thus providing a way for deriving consequences of sets of axioms in CASL specifications This is then extended to systems of rules for deriving consequences of structured specifications and for proving inclusions between classes of models of such specifications These systems are also used in rules for formal verification of the internal correctness of system designs as captured by architectural spec ifications For all these systems their soundness is proved and completeness discussed by reference to the formal semantics of CASL One point of interest is that again the extension of the basic proof system for consequences between sets of formulae to structured and architectural specifications does not really rely on the specifics of t
180. ned can be downloaded from the first one To maximize reuse each specification should be given only once in a single library In practice however libraries could be developed in parallel without collaboration and it might happen that a specification in one library is very similar to a perhaps differently named specification in another library When such duplication is noticed and the specification concerned is appropriate for general use the developers will be encouraged but not required to agree on using a common uniquely named specification defined in only one of the libraries Different versions of the same library are distinguished by hierarchical version numbers In practice specifications evolve e g to provide further operations or predicates on the specified sorts or to define new subsorts The libraries containing the specifications can evolve too by adding or removing named specifications Without some form of version control even a trifling change in one library might cause specifications in other libraries to become ill formed or affect their classes of models CASL allows different versions of the same library to coexist distinguishing them by hierarchical version numbers and allows downloadings in a library to indicate that a particular version of an other library is required Creation of new libraries is essential in connection with larger specification projects and projects of any scale can benefit
181. ns of such auxiliary symbols by using the local within construct This is illustrated in the above specification LisT ORDER where the insert operation is introduced only for the purpose of the axiomatization of order The operation insert has its scope limited to the part that follows within and is therefore not exported by the specification It is generally advisable to ensure that auxiliary symbols are declared in local parts of specifications Care is needed with local sort declarations spec LisT ORDER SORTED TOTAL ORDER with sort Elem pred _ lt sort Elem then local pred 1715 sorted List Ve e Elem L List e empty is sorted e cons e empty is sorted e cons e cons e L is sorted cons e L is_sorted e lt e within op order List List VL List e order L is sorted end The specification above is a variant of the specifi cation ORDER illustrating again the use of the local within construct this time to declare an auxiliary predicate Actually the two specifications are not equivalent since LisT ORDER SORTED is much looser and only requires that order L is a sorted list but perhaps not with the same elements as L spec WRoNG LisST ORDER SORTED TOTAL_ORDER with sort Elem pred _ lt __ sort Elem then local pred 715 sorted List sort SortedList L List e is_sorted L Ve e Elem L List e empty is_sorted e cons
182. ntended architecture of the implementation of the steam boiler control system C 1 Introduction The aim of this chapter is to illustrate how one can solve the Steam boiler control specification problem see Sec with CASL For this we provide a CASL specification of the software system that controls the level of water in the steam boiler Our work plan can be described as follows 1 The steam boiler control specification problem is reproduced in Sec This is a preliminary draft and various parts of it still need to be checked and polished Suggestions for improvements are most welcome as well as detailed comments on the specifications Somewhere a mention of Bidoit amp al paper in LNCS 1165 should be added 116 C Case Study The Steam Boiler Control System 1 The main task is to derive from the informal requirements a requirements specification written in CASL of the steam boiler control system In par ticular this task involves the following activities a We must proceed to an in depth analysis of the informal requirements Obviously this is necessary to gain a sufficient understanding of the problem to be specified and this preliminary task may not seem worth mentioning Let us stress however that the kind of preliminary anal ysis required for writing a formal specification proves especially useful to detect discrepancies in the informal requirements that would other wise be very difficult to detect Indeed from
183. o implement delete as sketched above since this specific implemen tation choice may not be compatible with an independently chosen realization for C where containers may be implemented by bags for instance In the case of the architectural specification since both containers and the delete operation are implemented in the same component CD we can of course decide to implement containers by lists without repetitions and delete as sketched above Thus the component D should expand amy given implementation C of NATURAL and provide an implementation of Cont_DEL which is tantamount to providing a generic implementation G of NATURAL which takes the particular implementation of Cont as a parameter to be expanded Then we obtain D by simply applying G to Genericity here arises from the independence of the developments of and D rather than from the desire to build multiple implementations of NATURAL using different implementations of a is reflected by the fact that G is left implicit in the architectural specification A unit can be implemented only if its specification is a persistent ex tension of the specifications of its given units For instance the component D can exist only if the specification NATURAL is a persistent extension of Conr NATURAL i e if any model of the latter specification can be expanded into a model of the former one which is indeed the case here Similarly the component
184. og 20 eer 20 sao MAUS dite dad 21 rc 21 21 mM 22 22 ea PRAT E 23 23 PIU Coa aed oot 24 160 Named Specifications DET UNION dae Sere os aes oe IM eR ena aes 25 25 Lr 27 SET PARTIAL 1 30 SET PARTIAL CHOOSE 30 TT 30 SET_PARTIAL_CHOOSE_3 31 81 32 TP 32 LAST SELECTORS 1 iere Tende hee beue da Ee PR Des 32 LIST SELECTORS 32 393 o hiw ak a E ERES CEDE 33 LAST SELECTORS 1 ui ha ee eps 33 Tre 33 won Mr c 34 OUTLET 34 TRITT 35 37 Me MI E 38 MEET 38 adu ad a aie Rae dd isi 39 Cdk aia died dil debit 40 vu Mr Lr 41 P Ere 41 42 tes feats aes 42 INTEGER 11 2 2 1 4 44 45 1 45 47 destined ang 48 eren 48 aida rptu dre en od adea Mo W
185. ollerState SoonFlow Unknown PCS free type Valpair pair low Value high Value ops mode State Mode nbSTOP State Nat status State x PhysicalUnit Status PS predicted State x PumpNumber ExtendedPumpState PCS predicted State x PumpNumber ExtendedPumpControllerState steam predicted level predicted State Valpair end We are now ready to provide the specification of the steam boiler control system considered as a labeled transition system We leave partly unspeci fied the initial state init since in our specification this state represents the state immediately following the receipt of the PHYSICAL UNITS READY message Hence intuitively the omitted axioms should take into account the messages sent and received during the initialization phase at least at the end of it It is therefore better to leave open for now the value of nbSTOP init status init PS predicted init pn PCS predicted init pn steam predicted init and level predicted init and to note that this would have to be taken care of when specifying the initialization phase The value of mode init is specified according to the end of Sec C 12 4 1 spec STEAM BOILER CONTROL SYSTEM SBCS ANALYSIS then op init State pred is step State x FinSet R Message x FinSet S Message x State Specification of the initial state init e mode init Normal V mode init Degraded Page 142 FIRST PUBLIC DRAFT 17 Sep 2
186. on normal de graded rescue emergency stop C 12 4 1 Initialization mode The initialization mode is the mode to start with The program enters a state in which it waits for the message STEAM BOILER WAITING to come from the physical units As soon as this message has been received the program checks whether the quantity of steam coming out of the steam boiler is really zero If the unit for detection of the level of steam is defective that is when v is not equal to zero the program enters the emergency stop mode If the quan tity of water in the steam boiler is above N2 the program activates the valve of the steam boiler in order to empty it If the quantity of water in the steam boiler is below then the program activates a pump to fill the steam boiler If the program realizes a failure of the water level detection unit it enters the emergency stop mode As soon as a level of water between N and has been reached the program send continuously the signal PROGRAM READY to the physical units until it receives the signal PHYSICAL UNITS READY which must necessarily be emitted by the physical units As soon as this sig nal has been received the program enters either the mode normal if all the physical units operate correctly or the mode degraded if any physical unit is defective A transmission failure puts the program into the mode emergency stop C 12 4 2 Normal mode The normal mode is the standard operating mode in which the p
187. on and try to understand the causes of the failure possibly detecting some flaw in the specification We will base our validation process on theorem proving i e we will check that some formulas are logical consequences of our requirements specifica tion For this purpose we use the tools described in Chap During this validation process we can consider two kinds of proof obligations 1 We can inspect the text of the specification and derive from this inspec tion some formulae that are expected to be logical consequences of our specification This can be considered as some kind of internal validation of the formal specification 2 We can check that some expected properties inferred from the informal requirements are logical consequences of our specification external val idation To do this we must first reanalyze the informal specification state some expected properties translate them into formulas and then Page 143 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 144 C Case Study The Steam Boiler Control System attempt to prove that these formulas are logical consequences of our spec ification This task is not easy since in general one has the feeling that all expected properties were already detected and included in the axioms during the formalization process The application of these principles to the requirements specification of the steam boiler control system leads to various proofs Below we give only a few il
188. on to add an observer related to the prediction of pump state messages The pre diction Open or Closed can however only be made when the status of the corresponding pump is OK This is why we extend the sort PumpState to introduce a constant Unknown PS Page 131 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 132 C Case Study The Steam Boiler Control System spec SBCS STATE 3 then free type ExtendedPumpState sort PumpState Unknown_PS P predicted State x PumpNumber ExtendedPumpState 4 status s Pump pn OK PS predicted s pn Unknown PS 196 end The specification of the detection of pump failures is now straightforward and is given in the PUMP FAILURE specification Remember that the meaning of Pump OK is only relevant when Transmission holds which in partic ular implies that for each pump there is only one PUMP STATE message for it in msgs Moreover we check the received value only if the predicted value is not Unknown PS spec PUMP FAILURE SBCS STATE 3 then pred State x FinSet RR Message x PumpNumber Vs State msgs FinSet R Message pn PumpNumber e Pump OK s msgs pn lt gt PS_predicted s pn Unknown_PS V PUMP_STATE PS predicted s pn as PumpState msgs end Let us now consider the detection of the failures of the pump controllers Again we rely on the predicted pump state controller message Here we must be a bit careful in order to reflect
189. one would be using a combination of NATURAL ARITHMETIC and INTEGER_ARITHMETIC see Chap 2 say by extending both in a structured specification see the next chapter for more details on structured specifications In such a combination a term such as suc 0 would have two parses one in sort Nat and one in sort Int in the absence of any subsort declaration relating Nat and Int and hence of any implicit embedding this term would then be ambiguous and would require explicit disambiguation to become a well formed term Page 44 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 5 3 Subsorts and Partiality 45 Supersorts may also be used for extending the intended values by new values representing errors or exceptions spec SET_ERROR_CHOOSE sort Elem sort Elem then sorts Elem lt ElemError op choose Set ElemError pred is in ElemError x Set VS Set e S empty choose S Elem choose S is in S end The above specification is another variant of the various specifications of sets equipped with a partial choose function given in Chap 4 This variant avoids the declaration of a partial function choose by using instead a supersort of Elem namely ElemError as the target sort of choose The idea here is that values of ElemError which are not embeddings of values of Elem represent errors e g the application of choose to the empty set Note that to obtain the desired effect it is necessary to explicitly
190. or each pump a device to measure the quantity of steam which comes out of the steam boiler an operator desk a message transmision system Page 149 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 150 C Case Study The Steam Boiler Control System C 12 2 1 The steam boiler The steam boiler is characterized by the following elements e A valve for evacuation of water It serves only to empty the steam boiler in its initial phase Its total capacity C indicated in litres The minimal limit quantity M of water in litres Below M the steam boiler would be in danger after five seconds if the steam continued to come out at its maximum quantity without supply of water from the pumps The maximal limit quantity of waters in litres Above the steam boiler would be in danger after five seconds if the pumps continued to supply the steam boiler with water without possibility to evacuate the steam e The minimal normal quantity of water in litres to be maintained in the steam boiler during regular operation M 1 e The maximal normal quantity N of water in litres to be maintained in the steam boiler during regular operation N lt Mg e The maximum quantity W of steam in litres sec at the exit of the steam boiler e The maximum gradient U of increase of the quantity of steam in litres sec sec e The maximum gradient Up of decrease of the quantity of steam in litres sec sec C 12 2 2
191. or that purpose and hide and reveal are just two symmetric constructs to achieve the same effect The use of reveal is il lustrated in NATURAL PARTIAL SUBTRACTION 4 above and the reader can convince himself that both NATURAL PARTIAL SUBTRACTION 3 and PARTIAL SUBTRACTION 4 export exactly the same symbols However in this case the first specification is clearly more concise A more convincing example of the use of reveal is provided by the following example spec PARTIAL ORDER 2 PARTIAL ORDER reveal pred lt end Page 51 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 52 6 Structuring Specifications Similar rules to the ones explained for renaming apply to the hide and reveal constructs One can qualify a symbol to be hidden or revealed by its kind sort op or pred and by default overloaded symbols are hidden or revealed simultaneously Note that hiding a sort entails hiding all the operations or predicates that use it in their profile Similarly revealing an operation or a predicate entails revealing all the sorts involved in its profile For instance in the specification above revealing the predicate lt entails revealing also the sort Elem As a consequence hiding sorts should be used with care in the presence of subsorts For instance hiding the sort Nat in the specification given in Chap 5 p leads to a specification of positive natural numbers with a sort Pos which h
192. ormed As a more complex example consider the following loose specification of an ordering function taken from Chapter 6 with sort Elem pred lt sort Elem then local pred is sorted List Ve e Elem L List e empty is sorted e cons e empty is_sorted e cons e cons e L is sorted cons e L is sorted e lt e within op order List List VL List e order L is sorted spec end The following specification of insert sort also is taken from Chapter 6 Page 77 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 78 10 Tools spec TOTAL ORDER with sort Elem pred lt sort Elem then local insert Elem x List List Ve e Elem L List e insert e empty cons e empty e insert e cons e D cons e insert e D when e e else cons e cons e L within op order List List Ve Elem L List e order empty empty e order cons e L insert e order L end Both specifications are related To see this we first inspect their signatures This is possible with hets g Sorting casl Hets now displays a more complex development graph see Fig 10 2 Here we have two types of nodes The named ones correspond to named specifications but there are also unnamed nodes corresponding to anonymous basic specifications like the above declaration of the insert operation above Again the simple solid arrows denote an ordinary import of specifications
193. our specification in case of misinterpretation The aim of the predicate Emergency is to characterize when we should switch to the EmergencyStop mode In Sec 12 4 2 it is said that the steam boiler control system should switch from Normal mode to Rescue mode as soon as a failure of the water level measuring unit is detected However in Sec 1214 4 it is explained that the steam boiler control sys tem can only operate in Rescue mode if some additional conditions hold represented by our predicate SystemStillControllable We decide there fore that when in Normal mode if a failure of the water level measuring unit is detected the steam boiler control system will switch to Rescue mode only if SystemStillControllable holds otherwise it will switch di rectly to EmergencyStop mode a sequence Normal Rescue EmergencyStop by a sequence Normal EmergencyStop Note that a sequence Normal Rescue Normal or Degraded is not possible since several cycles are necessary between a failure detection and the decision that the corresponding unit is again fully operational see Sec Page 124 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 C 4 Specifying the Mode of Operation 125 The axiomatization of the next mode of operation is now both simple and clear as illustrated by the MODE EVOLUTION 9 spec MODE_EVOLUTION preds Transmission State x FinSet R Message PU State x FinSet R Mess
194. pec PARTIAL ORDER 1 then implies Vr y z Elem e lt lt 2 1 lt 2 transitive end Display annotations should be provided at the beginning of a library see Chap 9 Page 9 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 10 3 Total Many Sorted Specifications The implies annotation above is used to emphasize that the transitivity of lt should follow from the other axioms or in other words that the model class of PARTIAL_ORDER_1 is exactly the same as the model class of PARTIAL Note however that an annotation does not affect the semantics of a specifi cation hence removing the implies annotation does not change the seman tics of the above specification but merely provides useful proof obligations The sole aim of an implies annotation is to stress the specifier s intentions and it will also help readers confirm their understanding Some tools may of course use such annotations to generate corresponding proof obligations here the proof obligation is PARTIAL ORDER 2 Elem e lt y y lt z lt z Discharging these proof obligations increases the trustwor thiness of a specification To fully understand that an implies annotation has no effect on the semantics the best is to consider an example where the corresponding proof obligation cannot be discharged as shown below spec IMPLIES_DOES_NOT_HOLD then implies Vz y Elem lt lt total
195. ple is similar in spirit spec NATURAL SUC PRE free type Nat 0 suc pre Nat end Page 33 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 34 4 Partial Functions Selectors are usually total when there is only one constructor spec PAIR sort Elem1 sort Elem2 free type Pair pair first Elem1 second Elem2 end While selectors are usually partial operations when there is more than one alternative in the corresponding datatype declaration they can be total and this is generally the case when there is only one constructor as in the above example The free datatype declaration entails in particular axioms asserting that first and second yield the respective arguments of the constructor pair i e first pair e1 e2 1 and second pair e1 e2 e2 Constructors may be partial spec PART CONTAINER sort Elem generated type P Container empty insert Elem P Container pred addable Elem x P Container vars e e Elem C P_Container e def insert e C addable e C pred isin Elem x P Container e e is in empty e e is in insert e C e V e is in C if addable e C end The intention in the above example is to define a reusable specification of partial containers The insert constructor is specified as a partial operation defined if some condition on both the element e to be added and the container C to which the element is to be added holds This condition
196. plex sys tem may be fairly large and should be structured into coherent easy to grasp pieces CASL provides a number of powerful specification building opera tions to achieve this as detailed in Chap 6 Moreover generic specifications described in Chap 7 provide pieces of specification that are easy to reuse in several contexts where they can be adapted as desired by instantiating them Specification building operations and generic specifications are useful to structure the text of the specification of the system under consideration How ever the models of a structured specification have no more structure than do those of a flat unstructured specification Indeed most examples given in the previous chapters could have been structured differently with the same meaning i e with the same models Structured specifications are usually ad equate at the requirements stage where the focus is on the expected overall properties of the system under consideration In contrast the aim of architectural specifications is to prescribe the in tended architecture of the implementation of the system Architectural speci fications provide the means for specifying the various components from which the system will be built and describing how these components have to be assembled to provide an implementation of the system of interest At the same time they allow the task of implementing a system to be split into in dependent clearly specified su
197. plicit fitting map is necessary The second parameter sort Elem2 of Page 61 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 62 7 Generic Specifications 18 instantiated by in this case a fitting symbol map must be provided since COLOUR exports two sorts RGB and CMYK Using the specification PAIR 1 would require us to write spec PAIR_NATURAL_COLOUR_1 NaTURAL ARITHMETIC and COLOUR fit Elem1 gt Nat Elem2 gt end which clearly demonstrates the benefit of using two parameters as in instead of just one as in PAIRI When parameters are trivial ones i e just one sort one can always avoid explicit fitting maps Consider for instance the following alternative to PATR spec PAIR NATURAL COLOUR 2 sort Nat sort RGB and and end This is particularly convenient when the argument specification exports several sorts Compare for instance spec Pos HOMOGENEOUS PAIR sort Pos and INTEGER 1 end and spec PAiR Pos 1 INTEGER ARITHMETIC 1 fit Elem gt Pos end Note that the instantiation NATURAL COLOUR fit Elem gt RGB is ill formed since it entails mapping the sort Elem to both Nat and RGB More generally care is needed when the several parameters of a generic specification share some symbols which in general is not advisable As a last remark note that it is easy to specialize a generic specification with several parameters as in the fo
198. ponent G to the combination denoted by and of C applied to N and of 5 applied to N This combination makes sense only if both C N and 5 N share the same interpretation of their common symbols their common symbols the sort Nat equipped with the operations 0 and suc all come from the same component N which provides their interpretation which is expanded hence cannot be modified in C N and in 5 N thus compatibility is guaranteed There is a clear analogy here between the application of the generic com ponent F with multiple arguments in and the com bination of C N and S N in SSE NV im beth cases the result is meaningful because we can trace shared symbols like the sort Nat and the operations 0 and suc to a single component N introducing them Let us emphasize again that compatibility is a natural requirement since each unit declaration corresponds to a separate implementation task and The braces and are not really necessary and are used to emphasize that has a single argument Page 213 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 214 8 Specifying Architectural Structure hence each unit subterm to an independently developed subsystem obviously the combination of components or unit terms makes sense only when some compatibility conditions are fulfilled Let us now consider an example where the compatibility condition is vio lated arch spec WRONG_ARCH_SPEC units CN
199. ponent is different from applications of several generic components with similar specifications t Elem RGB result FN N and FC C The above architectural specification is a variant of However in M one im plementation for containers in the generic component and then we apply it twice first to a component N implementing and then to a com ponent C implementing COLOUR In OT we may The situation is however a bit different with specification extensions which lead to specifications of generic components as explained above or to specifications of components expanding a given component as illustrated in the previous section Page 210 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 8 2 Explicit Generic Components 211 choose two different implementations for containers one for containers of nat ural numbers in the component F N and another one for containers of colours in the component FC The architectural specifications and are therefore similar but clearly different Neither is better than the other each corresponds to a different architectural decision and selecting one rather than the other is a matter of architectural design Components that are more widely reusable tend to have less efficient implementations in general Generic components may have more than one argument unit spec Busni GENeRaTED Ser ELE spec CONT2SET ELEM ELEM and Buen
200. portant to understand that the above overloading declarations are enough to achieve the desired effect and that no axioms are necessary The fundamental rule is that in models of CASL specifications with subsort ing embedding and overloading have to be compatible embeddings commute with overloaded operations This can be rephrased into the following intuitive statement If terms look the same then they have the same value in the same sort Thus our example the value of 1 1 is the same in Nat whatever the combination of the overloaded constant 1 and operation is chosen and there is no need for any axiom to ensure this since this is implicit in the semantics of subsorting Page 41 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 42 5 Subsorting 5 3 Subsorts and Partiality A subsort may correspond to the definition domain of a partial func tion spec POSITIVE_PRE then pre Pos Nat end Since we have introduced the subsort Pos of non zero natural numbers it makes sense to overload the partial pre operation on Nat by a total one on Pos as illustrated above to emphasize the fact that indeed pre is a total operation on its definition domain Note again that no further axiom is necessary and that the semantics of subsorting will ensure that both the partial and total pre operations will give the same value when applied to the same non zero value Using subsorts may avoid the need fo
201. r partial functions spec NATURAL POSITIVE ARITHMETIC free types Nat 0 sort Pos Pos suc pre Nat ops 1 Pos suc 0 Nat x Nat Nat assoc comm unit 0 Nat x Nat Nat assoc comm unit 1 Pos x Pos Pos Pos x Nat Pos Nat x Pos Pos Nat e z suc y suc z y 0 0 e suc y z x y end It is indeed tempting to exploit subsorting to avoid the declaration of par tial functions as illustrated by the above specification which is an alternative to PERO and avoids the intro duction of the partial predecessor operation Note that in the above example we have fully used the facilities for defining free datatypes with subsorts and This should not be confused with the same name same meaning principle which does not apply here the total pre and the partial one have different profiles and hence are just overloaded Page 42 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 5 3 Subsorts and Partiality 43 in particular non linear visibility for the declared sorts which allows us to refer to the subsort Pos in the first line before defining it in the second one Avoiding the introduction of the partial predecessor operation has some drawbacks since some previously well formed terms with defined values have now become ill formed e g pre pre suc 1 where pre suc 1 is a well formed term of sort Nat but pre expects an a
202. r program gmake file GT_pred make Then the generated C code is compiled with the following command gt gmake file GT_pred make Finally we get an executable file called a out This program computes the normal form of any query term gt a out Enter a query term of sort bool Page 84 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 6 Other tools 85 s s zero gt s zero end result true 10 5 ASF SDF Parser and Structure Editor for CASL ASF SDF was used to prototype the CASL syntaz The algebraic specification formalism ASF SDF and the ASF SDF Meta Environment have been deployed to prototype CASL s con crete syntax and to develop a mapping for the concrete syntax to an abstract syntax representation as ATerms BJKO00 The user defined also known as mixfix syntax of CASL calls for a two pass approach In the first pass the skeleton of a CASL specification is derived in order to extract user defined syntax rules In a second pass these syntax rules are used to parse the expres sions that using the mixfix notation Currently only the first pass is realized in SDF and the parsing is performed based on the underlying Scannerless Generalized LR parsing technology BSVV02 A prototype of the mapping from the concrete to abstract representation is written in ASF rewrite rules The ASF SDF Meta Environment provides syntaz directed editing of CASL specifications Given the concr
203. r reasoning applies to G More generally a generic component can be applied to any component or to any unit term that can be reduced along some morphism to an argument of the required type i e to a model of the required specification When necessary a fitting symbol map can be used to describe the correspondence between the symbols provided by the argument and those expected by the generic component We do not detail here the technicalities related to these fitting symbol maps since they are quite similar to those used in instantiations of generic specifications and the notations are the same As a last remark note that similarly to what happens when instantiating a generic specification by an argument specification when a generic component is applied to an argument richer than required the extra symbols are kept in the result Hence the result of the above architectural specification SYSTEM V contains also the interpretations of the arithmetic and ordering operations on natural numbers as they are provided by the component NA This means in particular that the implementation described by SvsTEM V has a larger signature than the one described by Specifications of components can be named for further reuse unit spec CONT COMP ErEM Conr ELEM unit spec CONT ETEN CoRT Dei Eis arch spec SvysTEM G1 result N In the above example we name the specification of generic
204. r set ASCII with optional use of ISO Latin 1 Key Words and Signs Reserved key words always lowercase and arch as assoc axiom axioms closed comm def else end exists false fit forall free from generated get given hide idem if in lambda library local not op ops pred preds result reveal sort sorts spec then to true type types unit units var vars version view when with within Reserved key signs gee m gt lt gt ja gt M A Unreserved key signs lt xX gt I Key words representing mathematical signs forall exists not in lambda V 1 A Key signs representing mathematical signs gt gt lt gt gt gt AV Identifiers Sorts and variables are simple words with digits primes and single under scores Y 297 A Rather Long Identifier select_1 Operations and predicates can also be sequences of signs unreserved and with any brackets balanced amp lt gt 7 8 771 7 emyl or single decimal digits 1234567890 or single quoted characters c The signs are not allowed in identifiers nor are the ISO Latin 1 signs for general currency yen broken vertical bar registered trade mark masculine and feminine ordinals left and right angle quotes fractions soft hyphen acute accent cedilla macron and umlaut Function and predicate identifiers can also be infixes prefixes postfixes and general mixfixes for
205. rary Basic Numbers 107 specify that two parts are equivalent if their differences are equal The sort Nat is then declared to be a subsort of Int Besides the division operator __ __ the specification INT also provides the function pairs div mod and quot rem respectively as constructs for di vision behaving differently on the negative numbers see V1 2 for a discussion The specification RAT of rational numbers follows the same scheme as the specification of integers discussed above This time the specification INT is imported The rationals are then defined as equivalence classes of pairs con sisting of an integer and a positive number written as quotients The sort Int is then declared to be a subsort of Rat Note that thanks to CASL subsorting the declaration of the operation Rat x Rat Rat allows writing rationals also as pairs x y of arbitrary integers and y 0 Again the definition of the predicates and operations on rationals usually covers the whole domain of rationals i e concerning consistency one has to show that they do not contradict to the axioms for naturals and integers to which they are related by overloading library BASIC NUMBERS 4 This library provides specifications of naturals integers and rationals Concerning the rationals the specification Rat includes the datatype proper while the specification DecimalFraction adds the notions needed to represent rationals as decimal fractions
206. re declared symbols at all This facilitates reordering library items and more importantly copying items between libraries Page 220 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 9 1 Local Libraries 221 Display parsing and literal syntax annotations apply to entire li braries library USERMANUAL EXAMPLES display __ lt __ LATEX display _ gt __ LATEX gt display union LATEX U prec lt left_assoc spec STRICT_PARTIAL_ORDER spec PARTIAL_ORDER STRICT_PARTIAL_ORDER then lt spec GENERATED SET sort Elem U spec INTEGER ARITHMETIC_ORDER lt gt Annotations affecting the way terms are written or displayed apply only to an entire library and have to be collected at the beginning of the library These annotations include display and precedence annotations illustrated above Recall that various reserved words and symbols in CASL specifications are input in ASCII but displayed as mathematical signs e g universal quantifi cation is input as forall and displayed as V when this sign is available in the current display format Display annotations provide analogous flexibility for declared symbols For example the display annotations illustrated above determine how infix symbols input as lt gt and union are displayed when using to format the specification Note that a display annotation applies to all occurrence
207. red to determine the exact relationship between parameters and arguments in instantiations and so called imports should be separated from the bodies of generic specifications 1 Generic specifications are also useful to ensure loose coupling between several named specifications of the same system replacing an explicit extension by a parameter including only the necessary symbols and their required properties This cannot however easily be illustrated in the framework of this User Manual 58 7 Generic Specifications 7 1 Parameters and Instantiation Parameters are arbitrary specifications Any specification named or not can be used as the parameter of a generic specification Commonly the parameter is a rather trivial specification con sisting merely of a single sort declaration as in most of the examples given in the previous chapters e g spec List_SELECTORS sort Elem However the parameter can also be a more complex possibly structured specification as in spec ToTAL_ORDER with sort Elem pred _ lt _ Recall that with requires the signature of the specification to include the listed symbols here in fact the signature of TOTAL ORDER does not contain any further symbols so those are all the symbols that have to be supplied when instantiating In instantiations the fitting of parameter symbols to identical argu ment symbols can be left implicit spec GENERIC COMMUTATIVE
208. red __ lt _ Elem x Elem pred abbreviates predicate Vzr y z Elem e r lt 1 strict lt gt lt r asymmetric 7 lt lt 2 gt 72 lt 2 transitive 4 Note that there may exist x y such that neither x lt y nor y lt x 96 end The above basic specification named intro duces a sort Elem and a binary infix predicate symbol lt Note that CASL allows so called mixfix notation i e the specifier is free to indicate using __ pairs of underscores as place holders how to place arguments when building terms single underscores are treated as letters in identifiers Using mixfix 1 Mixfix notation is so called because it generalizes infix prefix and postfix nota tion to allow arbitrary mixing of argument positions and identifier tokens Page 6 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 1 Loose Specifications T notation generally allows the use of familiar mathematical and programming notations which contributes substantially to the readability of specifications The interpretation of the binary predicate symbol lt is then constrained by three axioms A set of axioms is generally presented as a bulleted list of formulae preceded by the universally quantified declaration of the relevant variables together with their respective sorts as shown in the above example In CASL axioms are written in first order logic with equality using quantifiers and the
209. regoing chapters we have seen many examples of named specifica tions and of references to them in later specifications This chapter explains how a collection of named specifications can itself be named as a library The creation of libraries facilitates the reuse of specifications For practical appli cations it is important to be able to reuse at least existing specifications of basic datatypes such as those described in App Local libraries are self contained A library is called local when it is self contained i e for each reference to a specification name in the library the library includes a specification with that name Local libraries might appear at first sight to be all that we need but actually they provide poor support for reuse of specifications The problem is that when a specification from one local library is reused in another it has to be repeated verbatim There is no formal link between the original specification and the copy despite them having the same name the names used in a library can be chosen freely and different libraries could use the same name for completely different specifications Distributed libraries support reuse Distributed libraries allow duplication of specifications to be avoided al together Instead of making an explicit copy of a named specification from 218 9 Libraries one library for use in another the second library merely indicates that the specification concer
210. rgument of sort Pos The fact that pre suc 1 1 is a consequence of the specified axioms and that 1 is of sort Pos does not of course entail that pre suc 1 is of sort Pos too since axioms are disregarded when checking for well formedness See below for possible workarounds using explicit casts Moreover it is not always possible or easy to avoid the declaration of partial operations by using appropriate subsorts just consider e g subtraction on natural numbers As a last remark on this issue the reader should be aware of the fact that while overloading a partial operation on a supersort say pre on Nat with a total one on a subsort pre on Pos is fine overloading a total operation on a supersort with a partial one on a subsort forces the partial operation to be total and hence the latter would be better declared as total tooP Casting a term from a supersort to a subsort is explicit and the value of the cast may be undefined In CASL a term of a subsort can always be considered as a term of any supersort and embeddings are implicit On the contrary casting a term from a supersort to a subsort is explicit and since casting is essentially a partial op eration the resulting casted term may not denote any value Casting a term to sort s is written as s Consider the term pre pre suc 1 as Pos which is well formed in the context of the NATURAL POSITIVE fication This term
211. rogram tries to maintain the water level in the steam boiler between N and with all physical units operating correctly As soon as the water level is below N or above Ng the level can be adjusted by the program by switching the pumps on or off The corresponding decision is taken on the basis of the information which has been received from the physical units As soon as the program recognizes a failure of the water level measuring unit it goes into rescue mode Failure of any other physical unit puts the program into degraded mode If the water level is risking to reach one of the limit values M or Me the Page 152 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 12 The Steam Boiler Control Specification Problem 153 program enters the mode emergency stop This risk is evaluated on the basis of a maximal behaviour of the physical units A transmission failure puts the program into emergency stop mode C 12 4 3 Degraded mode The degraded mode is the mode in which the program tries to maintain a satisfactory water level despite of the presence of failure of some physical unit It is assumed however that the water level measuring unit in the steam boiler is working correctly The functionality is the same as in the preceding case Once all the units which were defective have been repaired the program comes back to normal mode As soon as the program sees that the water level measuring unit has a failure the program goes into mode rescue If
212. rol System As explained above in a first step we take care of the static analysis of the received messages and then in a second step we take care of the dynamic analysis of the received messages using how we have kept track of the status of the physical units i e using the observer status 3 Then for each physical unit we specify the detection of its failures by com paring the received message with the expected one For this comparison we can freely assume that the static analysis of the received messages has been successful i e that the message sent by the physical unit has been received The corresponding specifications are described in the next subsections C 5 2 Keeping Track of the Status of the Physical Units Remember that to perform the dynamic analysis of the received messages as explained above we must check that we receive failure acknowledgement and repaired messages when appropriate In order to do this we must keep track of the failures detected and of the failure acknowledgement and re paired messages received Since the same reasoning applies for all physical units we can do the analysis in a generic way For each physical unit we will keep track of its status which can be either OK Failure WithoutAck or Failure WithAck The status of a physical unit will then be updated accord ingly to the detection of failures and receipt of failure acknowledgement
213. ructors Page 26 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 A Partial Functions Partial functions arise naturally Partial functions arise in a number of systems CASL provides means for the declaration of partial functions the specification of their domains of definition and more generally the specification of system properties involving partial functions The aim of this chapter is to discuss and illustrate how to handle partial functions in CASL specifications 4 1 Declaring Partial Functions Partial functions are declared differently from total functions spec SET_PARTIAL_CHOOSE sort Elem sort Hem then op choose Set Elem end The choose function on sets is naturally a partial function expected to be undefined on the empty set In CASL a partial function is declared similarly to a total one but for the question mark following the arrow in the profile It is therefore quite easy to distinguish the functions declared to be total from the ones declared to be partial A function declared to be partial may happen to be total in some of the models of the specification For instance the above specification PARTIAL CHOOSE does not exclude models where the function symbol choose is interpreted by a total function defined on all set values Axioms will be 28 4 Partial Functions used to specify the domain of definition of a partial function and how to do this is detailed later
214. s __ a single underscore is a valid character in an identifier as illustrated in the above specification by the predicate symbol is n Loose datatype declarations are appropriate when further constructors may be added in extensions spec MARKING_CONTAINER sort Elem sort Elem then type Container mark_insert Elem Container pred _is_marked_in__ Elem x Container Ve Elem C Container e e is in mark insert e C lt e V e is in C e e is marked empty e e is marked insert e lt gt e is marked e e is marked in mark_insert e C e V e is marked end The above specification extends trivially instantiated by introducing another constructor mark insert for the sort Container hence values added to a container may now be marked or not Note that we heavily rely on the same name same thing principle here since it ensures that the sort Container introduced by the datatype declaration of CONTAINER and the sort Container introduced by the datatype declaration of are the same sort which implies that the combination of both datatype declarations is equivalent to type Container empty insert Elem Container mark insert Elem Container Note that since new values may be constructed by mark insert it is necessary to extend the specification of the predicate symbol is in by an extra axiom taking care of the newly introduced constr
215. s as a set does not imply that a set of received messages cannot contain several LEVEL v messages with distinct values for instance Hence we must check this explicitly Remember that receiving unknown messages 1 messages that do not belong to the list of messages as specified in Sec 126 is taken into ac count via the extra constant junk message see the specification MESSAGES RECEIVED We believe also that we cannot simultaneously receive a failure acknowledgement and a repaired message for the same physical unit 1 that Page 129 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 130 C Case Study The Steam Boiler Control System at least one cycle is needed between acknowledging the failure and repairing the unit We will check this as well 5 We focus now on the dynamic analysis of the received messages As explained above to perform this dynamic analysis we check that we re ceive failure acknowledgement and repaired messages when appropriate according to the current status of each physical unit We understand that for each failure signaled by the steam boiler control system the corresponding physical unit will send just one failure acknowledgement Moreover we will specify the steam boiler control system in such a way that when it receives a repaired message the steam boiler control system acknowledges it imme diately Hence if there is no problem with the message transmiss
216. s denote different values Hence a free datatype declaration as the one above has exactly the same effect as the similar generated datatype declaration together with axioms stating that suc is injective and that 0 cannot be the successor of a natural number An alternative to the above free type Nat 0 suc Nat is therefore generated type Nat 0 suc Nat Vz y Nat e suc y y Va Nat e 0 Free datatype declarations are particularly convenient for defining enu merated datatypes spec COLOUR free type RGB Red Green Blue free type CMYK Cyan Magenta Yellow Black end Using free instead of generated for defining enumerated datatypes saves the writing of many explicit distinctness assertions e g Red Green Red Blue Free specifications can also be used when the constructors are related by some axioms spec INTEGER free type Int 0 suc Int pre Int Int e suc pre z 2 x e pre suc x x end Page 18 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 3 Free Specifications 19 When some relations are to be imposed between the constructors as is the case here for suc and pre which are inverses of each other a free datatype declaration cannot be used since the contradiction between the no confu sion principle and the axioms imposed on the constructors would lead to an inconsistent
217. s of the input symbol in the library regardless of overloading Display annotations can give alternative displays for different formats apart from IATEX both RTF and HTML are presently supported The display of the annotation itself shows only the input syntax of the symbol and the result produced by the current formatter The input form of one of the above annotations might be as follows display __union__ HTML __ lt sup gt U lt sup gt LATEX __ cup__ When no display annotation is given for a particular format the input format itself is displayed Thus the symbol displayed as U in the present IXTEX version of this User Manual would be displayed as union in an RTF version unless the above annotation were to be extended with an RTF part Parsing annotations allow omission of grouping parentheses when terms are input A single annotation can indicate the relative precedence or the Page 221 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 This is consistent with the display annotations given in the basic libraries Should HTML be replaced by XHTML 222 9 Libraries associativity left or right of a group of operation symbols The precedence annotation for infix arithmetic operations given above allows a term such as b to be input and hence also displayed as a b c The left associativity annotation for and x allows a b c to be input as 0 and similarly for but the parentheses cannot be omitted
218. s s msgs Failure WithAck e status s Failure WithoutAck FAILURE_ACKNOWLEDGEMENT msgs gt next status s msgs Failure WithoutAck e status s pu FailureWithAck REPAIRED pu msgs gt next_status s msgs OK e status s pu FailureWithAck 5 REPAIRED pu msgs gt next_status s msgs pu Failure WithAck end C 5 3 Detection of the Message Transmission System Failures As explained above we first specify the static analysis of the received mes sages and then we specify the dynamic analysis of these messages To specify the static analysis of messages it is necessary to check that all indispensable messages are present In addition a set of received messages is acceptable if there are no duplicated messages in this set Since we have specified the collection of received messages as a set we cannot have several occurrences of exactly the same message in this set Note that this means that our choice of using sets instead of bags for instance is therefore not totally innocent either we assume that receiving several occurrences of exactly the same message will never happen and this is an assumption on the environment or we assume that this case should not lead to the detection of a failure of the message transmission system and this is an assumption on the requirements However specifying the collection of received message
219. sgs ps lt pn broken_pumps s msgs PUMP_STATE pn ps msgs within ops next_steam_predicted State x FinSet R Message Valpair chosen pumps State x FinSet R Message x PumpState FinSet PumpNumber 4 minimal pumped water and maximal pumped water cannot be made local since their specification relies on chosen pumps which must be exported 96 minimal pumped water maximal pumped water State x FinSet R Message Value level predicted State x FinSet R Message Valpair pred Dangerous WaterLevel State x FinSet R Message 9696 Axioms for STEAM Vs State msgs FinSet R Message pn PumpNumber e low nezrt steam predicted s msgs 2 0 low adjusted steam s msgs U2 x dt e high next steam predicted s msgs min W high adjusted steam s msgs U1 x dt 9696 Axioms for PUMPS e pn chosen pumps s msgs Open pn e reliable pumps s msgs Closed e pn chosen pumps s msgs Closed pn e reliable pumps s msgs Open e minimal pumped msgs dt x P x fi reliable pumps s msgs Open chosen pumps s msgs Closed e maximal pumped water s msgs dt x P x t reliable_pumps s msgs Open U chosen_pumps s msgs Open U broken pumps s msgs chosen pumps s msgs Closed 9696 Axioms for LEVEL e low nezt level predicted s msgs 0 low adjusted level s msgs minimal pumped water s msgs dt x U1 2
220. sitions of total functions with casting Page 45 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 6 Structuring Specifications Large and complex specifications are easily built out of simpler ones by means of a small number specification building operations In the previous chapters we have focussed attention on basic specifications and detailed how to use the various constructs of CASL to write meaningful but relatively simple specifications The aim of this chapter is to discuss and illustrate how to assemble simple pieces of specifications into more complex structured ones In particular we explain how to extend specifications make the union of several specifications as well as how to rename or hide symbols when assembling specifications Parametrization and instantiation of generic specifications are explained in the next chapter 6 1 Union and Extension Union and extension can be used to structure specifications spec Lisr SET sort Elem sort Elem and sort Elem then op elements of List Set Ve Elem L List e elements_of empty empty e elements_of cons e L e U elements of L end 48 6 Structuring Specifications The above example shows how to make the union expressed by and of two specifications see Chap 4 p 33 and GENERATED_SET see 3 16 and then further extend this union by some operation and axioms using then Union and extens
221. sorted The main advantage of using the local within construct is that the symbol s to be hidden are left implicit The convenience of this generally outweighs the danger of overlooking a locally declared sort that is needed for the profile of an exported symbol In any case CASL allows both styles and users can simply choose the one they prefer Page 54 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 6 5 Named Specifications 55 6 5 Named Specifications Naming a specification allows its reuse It is in general advisable to define as many named specifications as felt appropriate since this improves the reusability of specifications a named specification can easily be reused by referring to its name Not only do the names serve as abbreviations when writing specifications they also make it easy for readers to notice reuse Moreover when the name of a specification is aptly chosen e g readers may well be able to guess its signature and perhaps even the specified axioms from the name itself In Chap 9j we shall see how named specifications and other items can be collected in libraries and particular versions of them made available for use over the Internet References to named specifications are particularly convenient for specifi cations structured using unions and extensions where verbatim insertion of un named specifications would tend to obscure the structure When needed the signature of a r
222. st mention it without providing a new name as in with empty which is equivalent to with empty empty By default overloaded symbols are renamed simultaneously For instance in with __ __ gt plus all the five overloaded infix operations exported by see Chap 5 p are renamed into five plus operations with a functional syntax and the appropri ate profiles It is possible as well to reduce the overloading or to specifically rename one of the overloaded symbols by specifying its profile in the symbol map For instance NTEGER ARITHMETIC 1 with _ __ Pos x Pos Pos plus only the addition of two positive natural numbers is renamed into plus When combining specifications origins of symbols can be indicated spec LisT SET 1 sort Elem sort Elem with empty cons and sort Elem with empty U then op elements of List Set Ve Elem L List e elements_of empty empty e elements_of cons e L e U elements_of L end Since as explained above with empty cons means with empty empty cons cons identity renaming can be used just to emphasize the Page 50 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 6 3 Hiding 51 fact that a given specification exports some symbols This is illustrated in the specification above which is quite similar to but for the fact that here we emphasize that Lisr SELECTORS expor
223. t AV VALUE e SET MS fit Elem S Message V and SET MR V fit Elem R Message V and CST V end Page 145 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 We need total finite maps here The subsort TotalFinMap should be added to the finite map specification in the basic libraries 146 C Case Study The Steam Boiler Control System Here we decide to implement generic sets in a component SET reused both for sets of messages received and sets of messages sent Since the imple mentation of natural numbers is provided by the external component V we use V for the second argument of the generic component SET in the result unit term The specification of the components C and 5 of are simple enough that they do not need to be further architecturally refined However they are still not design specifications and hence the development is not fin ished yet For example the specification of the component 5 which implement the states of the steam boiler control system can be refined into the following specification which provides a concrete implementation of states as a record of all the observable values from Basic STRUCTUREDDATATYPES get FINMAP spec SBCS_STATE_IMPL then free type Status OK Failure WithoutAck Failure WithAck free type ExtendedPumpState sort PumpState Unknown_PS free type ExtendedPumpControllerState sort PumpControllerState SoonFlow Unknoun PCS free type Valpair
224. t val S end spec PAIR sort S sort T mono free type Pair S T pair first S second Page 109 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 110 B Basic Library end spec GENERATEFINSET sort Elem mono generated type FinSet Elem FinSet Elem Elem pred _ _ Elem x FinSet Elem a system of representatives for sort FinSet Elem is and x 1 x2 xn 9696 where x 1 lt x2 lt lt n gt 1 x iof type Elem for an arbitrary total order on Elem end spec FINSET sort Elem given NAT mono GENERATEFINSET sort Elem then def preds isNonEmpty FinSet Elem C FinSet Elem x FinSet Elem ops 40 Elem FinSet Elem I FinSet Elem Nat Elem x FinSet Elem FinSet Elem FinSet Elem x Elem FinSet Elem AN LU o7 _symDif FinSet Elem x FinSet Elem FinSet Elem end spec GENERATELIST sort Elem free type List Elem _ first Elem rest List Elem end spec List sort Elem given NAT GENERATELIST sort Elem then preds isEmpty List Elem Elem x List Elem ops List Elem x Elem List Elem first last List Elem Elem front rest List Elem List Elem i List Elem Nat List Elem x List gt List Elem reverse List Elem List Elem _ __ List Elem x Nat Elem take drop Nat x List Elem gt List Elem freq
225. tance so called free datatype declarations allow sorts and value constructors to be specified much as in functional programming lan guages using a concise and suggestive notation 6 3 Total Many Sorted Specifications CASL allows loose generated and free specifications The models of a loose specification include all those where the declared functions have the specified properties without any restrictions on the sets of values corresponding to the various sorts In models of a generated speci fication in contrast it is required that all values can be expressed by terms formed from the specified functions i e unreachable values are prohibited In models of free specifications it is required that values of terms are distinct except when their equality follows from the specified axioms the possibility of unintended coincidence between them is prohibited Section 3 1 below focusses on loose specifications Sect 3 2 discusses the use of generated specifications and Sect 3 3 does the same for free specifi cations Loose generated and free specifications are often used together in CASL each style has its advantages in particular circumstances as explained below in connection with the illustrative examples 3 1 Loose Specifications CASL syntax for declarations and axioms involves familiar notation and is mostly self explanatory spec STRICT PARTIAL ORDER 9696 Let s start with a simple example sort Elem p
226. tant in particular here data play a promi nent role in failure detection The various constructs provided by CASL allow the specifications to be formulated straightforwardly and perspicuously and significantly more concisely than in other algebraic specification languages As a last remark we must make clear that for the sake of simplicity the initialization phase of the steam boiler control system see Sec C 12 4 1 is not specified However it should be clear that it would be straightforward to extend our specification so as to take the initialization phase into account following exactly the same methodology as for the rest of the case study This chapter is organized as follows In Sec C 2 we start by providing some elementary specifications that will be useful for the rest of the case study In Sec we explain how we will proceed to derive the CASL requirements specification in a stepwise way Then in Sec we detail the specification of the mode of operation of the steam boiler control system In Sec we specify the detection of the various equipment failures and in Sec feral we explain how we can compute at each cycle some predicted values for the messages to be received at the next cycle In Sec C 9 we explain how our CASL requirements specification can be validated and in Sec we refine the CASL requirements specification in a sequence of architectural specifications that describe the intended architecture of the implementation o
227. tection of specifications and the insertion of usernames and pass words in URLs allows downloading between protected specifications With HTTP the username and password can be unrelated to those used for the host file system 9 3 Version control Libraries always have version numbers library BAsIC NUMBERS version 1 0 spes NAT spe INT then Spas RAT INT then As illustrated above a library can be assigned an explicit version num ber allowing it to be distinguished from previous and future versions of the same library CASL allows conventional hierarchical version numbers familiar from version numbers of software packages the initial digits indicate a major version digits after a dot indicate sub versions and digits after a further dot indicate patches to correct bugs Distinctions between alpha beta and other pre release versions are not supported Page 226 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 9 3 Version control 227 The smallest version number is written simply 0 and can be omitted when specifying the initial version of a library However the first installed version of a library could have any version number at all The numbers of suc cessively installed versions do not have to be contiguous nor even increasing e g a patched version 0 99 1 could be installed after version 1 0 Individual library items do not have separate version numbers Date anno tations can be us
228. the water level is risking to reach one of the limit values or the program enters the mode emergency stop A transmission failure puts the program into emergency stop mode C 12 4 4 Rescue mode The rescue mode is the mode in which the program tries to maintain a sat isfactory water level despite of the failure of the water level measuring unit The water level is then estimated by a computation which is done taking into account the maximum dynamics of the quantity of steam coming out of the steam boiler For the sake of simplicity this calculation can suppose that exactly n liters of water supplied by the pumps do account for exactly the same amount of boiler contents no thermal expansion This calculation can however be done only if the unit which measures the quantity of steam is itself working and if one can rely upon the information which comes from the units for controlling the pumps As soon as the water measuring unit is repaired the program returns into mode degraded or into mode normal The program goes into emergency stop mode if it realizes that one of the following cases holds the unit which measures the outcome of steam has a failure or the units which control the pumps have a failure or the water level risks to reach one of the two limit values A transmission failure puts the program into emergency stop mode C 12 4 5 Emergency stop mode The emergency stop mode is the mode into which the program has to go as we
229. the fact that stopping a pump has an instantaneous effect while starting it takes five seconds see Sec C 12 2 3 Since five seconds is unfortunately exactly the elapsed time between two cycles when we decide to activate a pump we may have to wait two cycles to receive a corresponding Flow pump controller state This is why in addition to the constant Unknown used for the cases where no prediction can be made since the pump controller is not working correctly we also introduce a constant SoonFlow to be used for the prediction related to a just activated pump spec 5 8 5 4 SBCS_STATE_3 then free type ExtendedPumpControllerState sort PumpControllerState SoonFlow Unknown_PCS op PCS_predicted State x PumpNumber ExtendedPumpControllerState 4 status s PumpController pn OK PCS predicted s pn Unknown PCS end The specification of the detection of pump controller failures is now straightforward and is given in the specifica tion Remember that the meaning of Pump Controller OK is only relevant Page 132 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 C 5 Specifying the Detection of Equipment Failures 133 when Transmission_OK holds which in particular implies that for each pump there is only one PUMP_CONTROLLER_STATE message for it in msgs Moreover we check the received value only if the predicted value is either Flow or NoFlow since if it is SoonFlow or Unknown PCS we cannot con clude
230. tion of the failures of the physical units On the other hand the steam boiler control system expects to receive or on the contrary not to receive some specific messages according to the history of the system for instance the steam boiler control system expects to receive a failure acknowledgement from a physical unit once it has detected a corre sponding failure and sent a failure message to this unit but not before and here some dynamic analysis is required Obviously the static analysis of the messages can be made on the basis of the received messages only while the dynamic analysis must take into account in addition to the received messages the history of the system and more precisely the history of the failures detected so far and of the failure acknowledgement and repaired messages received so far From this first analysis we draw the following conclusions on how to specify the detection of equipment failures 1 In a first step we should keep track of the failure status of the physical units This will lead to a new observer status on states and to a specifica tion STATUS EVOLUTION of how this status evolves i e of a status operation 2 Then we specify the detection of the message transmission system failures hence Transmission OK in the specification MESSAGE TRANSMISSION Page 127 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 128 C Case Study The Steam Boiler Cont
231. tly The rules regarding the omission of evident symbol maps in explicit fittings apply to named specification morphisms too Since a view is defined only when the given symbol map induces a spec ification morphism i e all models of the target specification when reduced along the signature morphism induced by the given symbol map provide models of the source specification it may be convenient to use views just to explicitly document the existence of some specification morphisms even when these are not intended to be used in any instantiation For instance the view INTEGER_AS_TOTAL_ORDER can be seen as the requirement that INTEGER_ARITHMETIC_ORDER indeed specifies lt to be a total ordering re lation and would therefore make sense even without being used later on in instantiations Views can also be generic view a AS Ke er es Elem e pr e Lok The above example illustrates again the use of view as a proof obliga tion since for the moment we do not have examples of generic specifications with as parameter Page 69 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 8 Specifying Architectural Structure Architectural specifications are meant for imposing structure on im plementations whereas specification building operations only structure the text of specifications As explained in the previous chapters the specification of a com
232. trol system actually stops Note also that we realize that the operation next nbSTOP is better specified in this MODE EVOLUTION specification Page 125 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 126 C Case Study The Steam Boiler Control System Degraded mode e Emergency s msgs Everything OK s msgs PU OK s msgs WaterLevel Transmission OK s msgs next mode s msgs Degraded 9696 Rescue mode e Emergency s msgs PU OK s msgs WaterLevel SystemStillControllable s msgs Transmission s msgs next mode s msgs Rescue 9696 nert nbS TOP e next_nbSTOP s msgs nbSTOP s 1 when STOP msgs else 0 end In the next step of our formalization process we will specify the predicates assumed by which amounts to specify the detection of equipment failures This will be the topic of the next section C 5 Specifying the Detection of Equipment Failures The detection of equipment failures is described in Sec 12 7 It is quite clear that this detection is the most difficult part to formalize mainly because both our intuition and the requirements see e g knows from elsewhere ncompatible with the dynamics suggest that we should take into account some inter dependencies when detecting the various possible failures For instance if we ask a pump to stop and if in the next cycle the pump state still indicates that the pump is open we may in principle infer either a
233. tructure of Hets will be clear in dashed arrow between the new nodes It states that insert sort acutally has September hopefully before the properties of a sorting algorithm It can be tackeled with the menu Here one can choose a theorem prover that shall be used the proof obligation or just state that one conjectures the obligation to be true Page 79 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 80 10 Tools List_Selectors Total_Order List_Order_Sorted Fig 10 3 Development graph for the two sorting specifications with view Page 80 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 10 3 HOL CASL 81 10 2 The CASL Tool Set and the Development Graph Manager MAYA Cats is needed as long as Hets does not support architectural specifi cations The CASL Tool Set Cats Mos00 is a precursor of Hets It comes with roughly the same analysis tools as Hets but does neither support extensions nor identify sublanguages of CASL The management of development graphs is not integrated in this tool but is provided with a different tool called MAvA which only supports part of CASL s structuring constructs Cats can be obtained under while MAYA is available under Cats and MAYA are mainly important because currently Hets does not support CASL architectural specifications yet However support of architec tural specifications is expected to be available within Hets in the near future 10 3 HOL
234. ts in partic ular the operations empty and cons and that GENERATED SET exports in particular the operations empty __ and U 6 3 Hiding Auxiliary symbols used in structured specifications can be hidden spec NATURAL PARTIAL SUBTRACTION 3 NATURAL PARTIAL SUBTRACTION 1 hide suc pre d en spec NATURAL_PARTIAL_SUBTRACTION_4 reveal Nat 0 1 lt end When writing large specifications it is quite frequent to rely on auxiliary operations and predicates to specify the operations and predicates of in terest Once these are defined the auxiliary operations are no longer needed and are better removed from the exported signature of the specification which should include only the symbols that were required to be specified This is the purpose of the hide construct Consider for instance the specification NATURAL_PARTIAL_SUBTRACTION given in Chap p Once addition and subtraction are defined the two basic operations suc and pre are no longer needed since suc z is more conveniently written z 1 and similarly pre x is expressed by x 1 and can therefore be hidden This is illustrated by the specification given above Depending on the relative proportion of symbols to be hidden or not in some cases it may be more convenient to explicitly list the symbols to be exported by a specification rather than those to be hidden The construct reveal can be used f
235. uctor Page 14 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 3 2 Generated Specifications 15 3 2 Generated Specifications Sorts may be specified as generated by their constructors spec GENERATED_CONTAINER sort Elem generated type Container empty insert Elem Container pred _is_in__ Elem x Container Ve Elem C Container e e is empty e e is in insert e C lt e V e is in C end When a datatype is declared as generated as in the above example the corresponding sort is constrained to be generated by the declared constructors which means that any value of this sort is built by some constructor applica tion This constraint is sometimes referred to as the no junk principle For instance in the above example having declared the datatype Container to be generated entails that in any model of any value of sort Container is denotable by a term built with empty insert and variables of sort Elem only As a consequence properties of values of sort Container can be proved by induction on the declared constructors A major benefit of generated datatypes is indeed that induction on the declared constructors is a sound proof principle The construct generated type used above is just an abbreviation for generated type and generated can be used around arbitrary signature declarations enclosed in and 2 Generated specifications are i
236. ust already be declared beforehand The specification sorts Car Bicycle Boat generated type Vehicle sort Car sort Bicycle sort Boat is more restrictive since the generatedness constraint implies that any value of the supersort Vehicle must be the embedding of some value of the declared subsorts Car Bicycle and Boat Intuitively the above datatype declaration means that Vehicle is exactly the union which again may not be disjoint of Car Bicycle and Boat In particular this declaration prevents subsequent Page 39 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 40 5 Subsorting introduction of further subsorts unless the values of the new subsorts are intended to correspond to some values of the already declared subsorts For instance if we were now to extend the above specification with sorts Plane lt Vehicle all values of sort Plane would have to correspond to Car Bicycle or Boat values which is presumably not what we were intending The specification sorts Car Bicycle Boat free type Vehicle sort sort Bicycle sort Boat entails the same generatedness constraint as in the previous example and moreover the freeness constraint requires that there is no common value in the subsorts of Vehicle Intuitively the above declaration means that Vehicle is exactly the disjoint union of Car Bicycle and Boat This means in par ticular that the introduction of a further common subsort of both Car
237. usual logical connectives The universal quantification preceding a list of axioms applies to the entire list Axioms can be annotated by labels written which is convenient for proper reference in explanations or by tools Note that V is input as forall and that is input as or The usual logical connectives gt A V and are input as gt lt gt and not respectively 7 can also be input directly as an ISO Latin 1 character The existential quantifier q is input as exists It is advisable to comment as appropriate the various elements introduced in a specification The syntax for end of line and grouped multi line comments is illustrated in the above example The above STRICT_PARTIAL_ORDER specification is loose in the sense it has many non isomorphic models among which models where lt is inter preted by a total ordering relation and models where it is interpreted by a partial one Specifications can easily be extended by new declarations and axioms spec TOTAL_ORDER then Vz y ex lt yVy lt Vr y total end Extensions introduced by the keyword then may specify new symbols possibly constrained by some axioms or merely require further properties of old ones as in the above TOTAL_ORDER example or more generally do both at the same time In TOTAL ORDER we furth
238. vel is risking We will therefore assume that the specification SBCS_ANALYSIS will pro vide the following predicates which given a known state and newly received messages should reflect the failures detected by the steam boiler control sys e Transmission_OK State x should hold iff we rely on the message transmission system e PU_OK State x FinSet R_Message x Physical Unit should hold iff we rely on the corresponding physical unit e DangerousWaterLevel State x FinSet R Message should hold iff we estimate that the water level risks reaching the min M1 or max M2 limits However at this stage our understanding of the steam boiler control system is still quite preliminary and it is therefore too early to attempt to specify these predicates Therefore our specification MODE EVOLUTION where we specify the new operating mode according to the previous one and the newly received messages i e the operation nert mode will be made generic w r t these predicates Let us emphasize that here genericity is used to ensure a loose coupling between the current specification of interest and other specifications expected to provide the needed predicates Let us now explain how to specify the new mode of operation At first glance the informal requirements see 12 4 look quite complicated mainly because they explain for each operating mode under which conditions the steam boiler
239. why we have preferred a more verbose axiomatization of the predicate is_in Note also the use of the keyword if to write an implication in the re verse order is_in insert e S if e is_in S is equivalent to e S gt e is in insert e S The following example specifies the transitive closure of an arbitrary binary relation R on some sort Elem both provided by the parameter spec TRANSITIVE CLOSURE sort Elem pred _R__ Elem x Elem free pred _Rt__ Elem x Elem Vz y z Elem e Rtz gt 2 Rtz In the above example it is crucial that predicates hold minimally in models of free specifications since this property ensures that what we define as RP is actually the smallest transitive relation including R Without requiring the freeness constraint one would allow arbitrary relations containing the transitive closure of R and these undesired relations cannot be eliminated merely by specifying further axioms Loose extensions of free specifications can avoid overspecification spec NATURAL_WITH_BOUND then maz_size Nat axiom 0 lt maz_size end The above example shows another benefit of mixing loose and initial se mantics Assume that at this stage we want to introduce some bound of sort 8 If an element e belongs to a set 5 then this set S can always be denoted by a constructor term of the form insert e S due to the axioms constraining the constructor
240. y to predicate symbols While in most cases using compound identifiers for sorts will be sufficient in some situations it is also convenient to use them for operation or predicate symbols as done here for order lt When is instantiated not only the sort List Elem gets renamed here List Int but also the operation symbol order __ lt according to the fitting symbol map corresponding to the instantiation If we would not have used a compound identifier for the order operation then an unintentional name clash would have arisen Note that on the other hand we rely on the same name same thing principle to ensure that the sorts List Int provided by each of the two instantiations are the same which indeed is what we want for this example Page 65 FIRST PUBLIC DRAFT 17 8ep 2003 17 54 Tentative section title 66 7 Generic Specifications Of course we do not bother to use a compound identifier for the insert operation symbol This operation being local it is not exported by and cannot be the source of unintentional name clashes in in stantiations 7 3 Parameters with Fixed Parts Parameters should be distinguished from references to fixed specifica tions that are not intended to be instantiated spec LisT WEIGHTED ELEM sort Elem op weight Elem Nat given NATURAL ARITHMETIC Lisr REV sort Elem then op weight List Elem Nat Ve Elem L List Elem e weight empty 0
241. ying Architectural Structure RGB and CMYK Finally both application results are combined which is expressed by and Apart from free all specification building operations for structured spec ifications have natural counterparts at the level of components which are expressed using the same keywords The reader should remember that specification building operations work with specifications defining classes of models e g union of specifications denoted by and while in architectural specifications we work with individual models corresponding to components as is the case here inl OTHER SYSTEM where and denotes the combination of two components Similarly to union renaming and hiding have natural counterparts at the level of components For instance remember that the implementation de scribed by has a larger signature than the implementation de scribed by SvsTEM G It is however easy to modify the result part of TEM V if what we really want is an implementation with the same signature as the implementation described by SvsrEM one has just to hide the extra symbols resulting from the component NA as follows result F hide lt 1 c or result G F NA hide _ lt _ 1 c Symbol maps used in renaming and hiding at the level of components follow the same rules as symbol maps used in renaming and hiding at the level of structured specifications see Chap 6 Several applications of the same generic com
242. yped and references to named entities are in scope Then the model semantics takes a well formed CASL specification and assigns a model theoretic meaning to it CASL specifications denote classes of models In CASL well formed specifications denote signatures static semantics and classes of models model semantics Basic specifications which in essence present a signature and a set of axioms over this signature denote the class of models that satisfy all the axioms The semantics of basic specifications is split into two parts first many sorted basic specifications are described Chap III 2 and then features for defining and using subsorts are added Chap II 3 The semantics is largely institution independent A few more concepts are needed to explicate the semantics of structured specifications Chap IIL4 Key here is the notion of signature morphism and the model reducts and translation of sentences that signature morphisms induce Having introduced those we obtain the institution of CASL One important point of the semantics is that all the layers of the semantics above basic specifications are institution independent i e well defined for any institution chosen to build basic specifications as long as the institu tion comes with a bit of extra structure concerned with forming unions of signatures and defining signature morphisms see Sect III 4 1 Next we have the semantics of architectural sp
243. ys considered as an implicit extension of SP1 and SP1 SP2 abbreviates SP1 SP1 then SP2 Moreover since the generic component GC should expand any model of SP1 the specification SP1 5 2 is consis tent 1 has some models if and only if the specification SP1 then SP2 is a persistent extension of SP1 Forgetting this fact is a potential source of incon sistent specifications of generic components in architectural specifications For instance the specification NATURAL NATURAL is inconsistent for the reasons explained at the end of the previous section A generic component may be applied to an argument richer than re quired by its specification arch spec SYSTEM_V Nara The above architectural specification SYSTEM V is a variant of Here we require a component NA implementing the specification URAL_ARITHMETIC instead of a component N implementing NATURAL as 1 When SP2 is already defined as an extension of SP1 as it is the case for instance here for Cont_DEL NATURAL SP2 is equivalent to SP1 then SP2 Page 207 FIRST PUBLIC DRAFT 17 Sep 2003 17 54 208 8 Specifying Architectural Structure in perhaps because we know that such a component is already available in some collection of previously implemented components The generic component requires a component fulfilling the specification but can of course be applied to a richer argument as in F NA A simila

User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents