GRAPHIC SPECIFICATION OF ABSTRACT DATA TYPES
- 格式：pdf
- 大小：287.81 KB
- 文档页数：9
REVISTA FACULTAD DE INGENIERÍA, U.T.A. (CHILE), VOL 12 N°1, 2004, pp. 15-23GRAPHIC SPECIFICATION OF ABSTRACT DATA TYPESPedro Rossel 1 Ricardo Contreras 2María Cecilia Bastarrica 3Recibido el 5 de diciembre de 2003, aceptado el 7 de mayo de 2004RESUMENLa definición formal de requisit os de soft ware usando especificaciones algebraicas t iene t odas las vent ajas de lasespecificaciones formales y su sólida base teórica. Este tipo de especificaciones es generalmente textual. La mayor parte de los lenguajes de especificación modernos tienen una representación gráfica para mejorar su usabilidad. Esto también es el caso de las especificaciones algebraicas. En este artículo presentamos una recopilación de las formas en que los tipos abstractos de datos pueden ser representados gráficamente usando especificaciones algebraicas, proponiendo una notación que incluye el conjunto de todas las facetas encontradas en la literatura. También mostramos un ejemplo de aplicación y algunos resultados experimentales de usar esta notación gráfica en la práctica.Palabras Claves: Ingeniería de software, métodos formales, especificación algebraica, tipos abstractos de datos.ABSTRACTFormally specifying sof t ware requiremen t s using algebraic specifica t ions has all t he advan t ages of formal specifications. This t ype of specificat ions is usually textual. Most modern specificat ion languages have a graphical representation in an attempt to improve usability. This is also the case for algebraic specifications .Here we present a survey on how abst ract dat a t ypes are represent ed graphically. We propose a st ruct ure cont aining a superset of all elements surveyed. We also show an application example, and we report some experimental results when using this graphical representation.Keywords: Software engineering, formal methods, algebraic specification, abstract data types, graphic language.1 Universidad Católica del Maule, Departamento de Computación e Informática. Av. San Miguel 3605 Talca, Chile, prossel@hualo.ucm.cl2Universidad de Concepción, Depart ament o de Ingeniería Informát ica y Ciencias de la Comput ación. Edmundo Larenas 215 Concepción, Chile, rcontrer@inf.udec.cl 3Universidad de Chile, Departamento de Ciencias de la Computación. Blanco Encalada 2120 Santiago, Chile, cecilia@dcc.uchile.clINTRODUCTIONThe first and perhaps t he most import ant st ep for t he success of he sof ware developmen process is he requirements specification. This is critical because it is common t o in roduce mis akes hat are difficult and expensive to remove afterwards. There are several tasks in requiremen t trea tmen t: requiremen telici t a tion, writing these requirements as a consistent, complete and non-ambiguous documen , and requirement s analysis. Writing requirement s is usually known as requirement specification; different notations have been proposed for this purpose ranging from unst ruct ured and informal tex t to highly formal ma t hema t ical no t a tions. The approach used in each case depends on the goals of the project and the available resources. Informal specifica ions are easy o develop but t hey provide very lit le support for syst em analysis. In t his way there is no cer t ain t y t ha t specifica tions are complete, non-ambiguous, or t hat t hey fulfill all t he desired charact eristics of funct ional or non-funct ional requirements. However, mos tpeople use informal specifications because formal me t hods are still perceived as more difficult and expensive, even though it has been largely proven that this is not true [3], [6], [8], [13]. Formal specificat ions may require a longer specification time and expert personnel, but they allow and suppor t specifica t ion analysis and they reduce testing effort. Algebraic specifications are a formal way of specifying software systems as heterogeneous algebra's, i.e. a series of set s over which some operat ions are defined [10]. This t echnique has been developed for t he last t hree decades and it is widely known. Besides formalit y, specificat ions can also be classified as ei t her t ex tual or graphical. Traditionally, specifications were textual and this allowed a lot of fine grained detail to be specified. However, it is difficult to grasp the meaning of the whole system just looking at aPedro Rossel, Ricardo Contreras, María Cecilia BastarricaRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 200416textual specifica t ion, so effor t s have been made t o develop visual no a ions o overcome his difficul y. Graphical specifica t ions are generally clearer than textual specifications, but they are also less scalable.Fig. 1.- Classification of requirements specificationsThe ex ual or graphical charac eris ic is or hogonal with respect to the formality of the specification. In this way we may have all combinations as shown in Fig. 1. Algebraic specifica ions are ypically t ex tual, bu in recent years there has been an effort towards specifying them graphically. Therefore, we can count on all t he theory behind algebraic specifications while gaining the usability provided by graphical notations. Formal and Informal SpecificationsThere are wo ex reme ways of specifying sof ware requirements: a complet e formal specification and an informal specifica t ion. There also exis tsome intermediate represen t a tions t ha t have shown t o be useful in pract ice more as a means of communicat ion between users and specialis ts than as requirement specification languages. These semiformal notations have also been used for document ing design, probably because t here is no s t andard no t a t ion, nei ther for requirements nor for design. Table 1 is t aken from [9] and i t shows differen t ca t egories in formali t y and examples in each category.In order to have a formal requirements specification we need a formal specifica t ion language. A formal specification language provides a no t a t ion (syn t ax domain), an object universe (semantic domain), and the definition of precise rules about which object sat isfies the specification [23]. Table 1.- Classification of notationst tt t t t t tt t tt Textual and Graphical Specifications A graphical specificat ion is one whose element s arevisual, rather that textual. Despite the linguistic parallel, however, graphical specifications are not easily relat ed to heir ex ual coun erpar s even in very simple problems. Impor an effor s are devo ed in current research to this correspondence.In many cases, people perceive information easier when i is presen ed in a graphic form. Given he comprehensive advant ages of pict orial represent at ions for people not t rained in formal met hods, some effort s have been made to establish a bridge between this kind of users and rigorous formal users. In [17], a language for specificat ion of high level propert ies of real t ime systems is present ed, based on t emporal logic, and t o hide obscure formal notation to users, authors employ a two-level approach allowing user-level expression s t ohave a graphical not at ion. In t his work t he idea of a bridge is implemented by considering this approach as a natural division of responsibilities. The use of templates is a par ially cons ruc ed formula of he underlying temporal logic, similar t o t he t emplat es we present for graphic notation.Algebraic specifications are generally t ext ual, but there have been some at empt s t o make t hem graphical in order to gain usability and to shorten the learning curve.Graphic specification of abstract data typesRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 2004 17In a very int erest ing work, Neary and Woodward [18] address t he problem of comparing t he rela t ive comprehensibility of one t ext ual and t wo visual forms of algebraic specifica t ions. This comparison uses a small specificat ion present ed t o a t est group, and t hey conclude ha he graphical formalisms are easier t o manage for novice users.The PaperIn t his paper we presen tan overview of algebraic specification of abst ract dat a t ypes (ADTs) and t heir graphical represent at ion. We also show an applicat ionexample. Fig. 2 sets the context of its contents.Fig. 2.- Paper context The nex t Sec t ion presen ts how ADTs are formally specified using algebraic specifications; it also presents its most relevant characteristics. Then, we show how a simple information system can be specified using ADTs showing both a textual and a graphical version. Finally, we report the result s of our experience using graphical ADTs and presents some conclusions. ABSTRACT DATA TYPES SPECIFICATION An abstract data type can be considered as a black box, where users can only see the syntax and semantics of its operations. ADT operarations can be classified as either constructors or inspec ors [2]. Fig. 3 illus ra es his feature. Operations on the left hand side of the figure are used for const ruct ing object s. Those on t he right hand side, access and test, are used for querying information from an abs t rac t objec t , and modifica tion changes ADTs internal data [2]. Algebraic specifica ion is a formal me hod used for software requiremen t s specifica tion. They are used since t he 1970's as a t echnique for dealing wit h dat a structures in such a way t hat is independent from their implementation [6], providing a common description for data st ruct ures and operat ions t hat apply t o t hem [2]. Algebraic specifications are natural for defining ADTs.Fig. 3.- ADT SpecificationThe rela ionships among opera tions in an ADT are defined wi t h equa t ions generally called axioms, between t erms buil t using bo t h cons t an t s and the aforementioned opera t ions. Each t erm represen t s an abstract object and an equation specifies that two terms represen he same objec . Axioms are he seman ic essence of algebraic specifications [2].There are several approaches to algebraic specifications, which differ more in the form than in content, as it can be seen in [2], [4], [10], [12], [22], [24]. This art icletakes the perspective given by [4] and [12], adding someelements t hat support t he charact erist ics of t ransact ion processing syst ems [20]. We also enrich t he set E t oinclude not only axioms but also the whole semantics of the defined ADT. Formally, an algebraic specification is identified in [6], [7] as a triple: SPEC = {S ; OP ; E} (1) where: S : set of abstract data types, OP : set of constant and operation declarations, E : set of equations or axioms. Notation The st ruct ure of an algebraic ADT specificat ion may contain the following elements: ADT name : Beginning of t he specificat ion, where t he ADT name is indicated. IMPORT : Specifies other ADTs that can be used in the present specification.Pedro Rossel, Ricardo Contreras, María Cecilia BastarricaRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 2004 18TUPLES : Declares a locally defined dat a ype, t hat may be composed of a series of fields. Types declared in TUPLES can be used in the current specification for defining variables, as well as in all ADTs t hat import the current ADT. SYNTAX : Opera t ion signa tures are specified by including their name, domain and range. SEMANTICS : Section formed by five subsections that define: VARIABLES, AXIOMS, SEQUENCES, DATA and PREDICATES. These part s give meaning t o t he operations declared in SYNTAX, and also s a e he constraints and condi t ions where they are valid. SEQUENCES are used to constrain the order in which operations must be accomplished; the operat ion on the left of the >> sign must be performed before the one on the right. VARIABLES is used to define local variables. DATA const rains t he values t hat variables can t ake; interval values can be est ablished, or const ant s wit h values of other variables previously restricted in DATAcan be considered. AXIOMS are present in almost all algebraic specificat ion languages. PREDICATES adds another level of cons t raining opera t ion defini t ion. AXIOMS are expressed t hrough equa tions while PREDICATES establish certain properties through first order logic assertions. END ADT : Indicat es t he end of t he abst ract data t ype specification. The elemen ts name, SYNTAX and AXIOMS are identical o hose used in [4], [12], [22], [24]. The element IMPORT is used in [4], [12], [22] and TUPLES appears in [12]. SEMANTICS can be found in [4], but only in a rest rict ed format. VARIABLES is used as in [4], [12], [24]. SEQUENCES can be found in [5], [24]. DATA is not used in any of the algebraic specification languages reviewed, bu t i t fur t her specifies and constrains t he values variables can t ake. We use t he syntax given by [24] for the PREDICATES. The formal syntax of each specificat ion element is given in t he Appendix. These specification elements were chosen because they provide the expressiveness we need for specifying information syst ems charact erist ics, while st ill keeping the specifica t ion simple. All of t hem are formally defined and they allow us to specify both functional and non functional requirements. A Graphic Specification for ADTsWe propose to use a graphic notation for some parts of the ADT specifica tion including the same elemen ts defined in t he tex tual algebraic specifica tion. The elements and s t ruc t ure of t he graphic specifica t ion language are a synt hesis of t he proposals of [1], [5],[14], [15]. The textual algebraic specification languageis isomorphic wi t h t he graphic language, so each element of one language has a correspondent element in the o t her one, and t his correspondence is unique. Correspondence bet ween bot h languages is shown in Table 2. This t able also shows t he synt ax of graphicalelements.In the proposed graphic language, each ADT is defined by wo diagrams: one general diagram including alldescribed elemen t s, bu tSEQUENCES, and ano t her diagram including only the SEQUENCES diagrams. We chose to put SEQUENCES in another diagram to make the specification clearer; each operation may participatein several sequences, making i qui e complex. Forelements VARIABLES, DATA and PREDICATES we still use only the textual notation. All these features areillustrated in t he example in Sec tion EXAMPLE:INFORMATION SYSTEMS . CharacteristicsGraphic specificat ions have some virt ues t hat are notvery obvious in a t ext ual specificat ion, alt hough t hey could be presen t . We here discuss some of t headvantages of having both, a textual and a graphic dual specification. ModularityIn the context of an ADT graphic specification, an ADT can be seen as a module, which in an isolat ed way ignores t he det ails and specificat ion of ot her modules. For a specific ADT, it is not necessary to make explicit the specifica t ion of t hose ADTs in IMPORT and TUPLES. However, in order t o int egrat e a complet e system, we should also consider the relationship among these modules. In order to have a modular specification it is necessary to have a consist ent specificat ion wit hin t he ADT and with respect to other ADTs specification [20]. Hierarchy Modularity is not enough t o manage complexit y. We need to be able to deal with abstraction and hierarchical specifications in a common approach. Our notation can deal with hierarchical specifications mainly through theIMPORT and TUPLE sections. When an ADT2 is import ed by an ADT1, ADT1 may use t he operat ions and definit ions of t he ADT2, under the cons rain s ha ADT1 may impose. If here areGraphic specification of abstract data typesRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 200419several hierarchical levels, the higher ones can use t heoperations defined in all lower level ADTs.ScalabilityGraphic specifica t ions t end t o be more in t ui t ively understandable t han textual specifications; however, asthe complexit y of t he syst em grows, t his charact erist icdecreases rapidly. Having a dual t extual and graphic notation allows us o use graphic specifica ions for small and simple pieces, but we can still use the textual notation for very complex ADT specifica ions. Even though, this is generally accepted as true, we can use the modularity and hierarchical proper t ies to keep allspecifications as simple as possible, and continue usingthe graphic no t a t ion as t he comple t e sys t emspecification grows in size and complexity.LearningIn general, we can say t hat the brain does not code and internalize informa ion unless i finds i significan . Relevan t informa t ion is t hen re t ained t hrough a memorization process [11], [25].Long term memory is essential for the learning process[25]. This memory s t ores informa ion in associa ionnetworks organized in a hierarchical way [11]. Thus, using diagrams for graphical specifica t ion, wi th modularity and hierarchy charac t eris t ics as t hosepresented in t his article, makes it easier t o have t hem coded in memory, and so it implies an easier use and a faster learning process.EXAMPLE: INFORMATION SYSTEMSIn t his work, we considered t he specifica tion of information sys t ems, i.e. t ransac t ion processing systems. This kind of systems stands for most of the real world applicat ions [16], [21], so it is an int erest ing application domain. Transaction processing sys t ems include several ac t ivi t ies, mainly da t a s t orage, da ta processing according t o business rules, user int erface, and da a recovery; i may also add a programming interface to allow for extensibility. Fig. 4 illustrates the type of interactions expected for this kind of systems.According t o [19] and [22], informat ion syst ems have requirements of diverse na t ure: func tional, non-functional, hardware, e t c. For t his work we focussed on funct ional requirement s and some of t he possible non-functional requirements, such as operationprecedence, data representation, and constraints on data values.Table 2.- Correspondence between languagestPedro Rossel, Ricardo Contreras, María Cecilia BastarricaRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 200420I N P U TO U T P U TI N P U TFig. 4.- Data Storage and Recovery SystemFig. 5.- Textual Algebraic Specification of ADT ToartIn order o show he applica ion of he proposed specification languages, a simple information system is specified. The system name is “TOART” (TO ARTicle) and it allows to register the papers and books used in the preparation of a scient ific art icle. This syst em should have funct ionalit y for the insert ion, deletion and query of books and art icles. The syst em should be able t o answer at least two questions (functional requirements):• Which books did certain author write? • Which articles did certain author write?The ex ual algebraic specifica ion of he sys em is formed by three ADTs: Toart , described in Fig. 5, Book_Collection , in Fig. 6, and Article_Collection , similar o Book_Collection . ADT Toar imports and uses the other two in its specification.In ADT Toart , t he operat ion consult_book_by_author returns the book or books that certain author has written. Similarly, consult_article_by_author ret urns t he art icle or art icles writ t en by t he aut hor. In t he case of ADT Book_Collection , he opera ion enter_book inserts a new book in o he collec ion, and opera ion eliminate_book deletes a book from the collection.Data types such as Boolean, Natural, Integer and String, are predefined as par of he algebraic specifica ion language. Document_Author and Document_Name are imported by Book_Collection and Article_Collection and they are assumed to be defined elsewhere. Fig. 6.- Textual Algebraic Specification of ADT Book_CollectionThe graphic specificat ion of t he syst em cont ains t hree diagrams, one for each ADT. The ype diagram for ADT Toart is shown in Fig. 7. Sequence diagrams in Fig. 8 also belong to ADT Toart .Graphic specification of abstract data typesRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 2004 21Fig. 7.- Graphic Specification of ADT Toart Fig. 8.- Graphic Specificat ion of t he Sequences inADT ToartEven t hough t he syst em specified in t he example issimple, it shows all t he specificat ion element s in t hetextual and graphic languages. We can in t ui tivelycompare t he unders t andabili t y of bo th approaches,where it is clear that it is easier to ident ify operat ions, axioms and sequences in t he graphic not at ion, but we can also see that graphic notation is less scalable whenthe specification is long and complex.CONCLUSIONSAlgebraic specifica t ions are t radi t ionally t ex t ual but they can also be specified graphically. Many approaches have been proposed in t his direct ion. We present ed a superset of all the features proposed in order to show thepotential expressiveness of t he t echnique, includingthose especially sui t ed for specifying t ransac t ionalsystems. As it happens wit h most graphical notations, graphical ADTs allow us o get a general underst anding of a system easier than the textual specification for the same system. However, developing the most complex parts of the specificat ion as axioms or predicat es remains veryclose t o t ex t or comple t ely t ex t ual, so t here is noimprovement. We have had the experience of applying this two formsof algebraic specifica t ions for t wo semes t ers for teaching formal me t hods t o four t h year compu t er science st udent s. They unanimously declared t hat t he graphical form was easier to understand than its textual isomorphic specificat ion. Even t hough t his was not acontrolled experiment, it gives us some intuition about the usabilit y and underst andabilit y of graphical ADTspecifications.As expected, a graphical isomorphic representation of a textual algebraic specifica t ion can only improve understandability, even t hough it does not remove t hecomplexity of developing the specification.REFERENCES[1] H. Ben-Abdallah, I. Lee, and J.Y. Choi; “GSCR: a Graphical Language with Algebraic Semantics forthe Specifica t ion of Real-Time Sys t ems”. Technical repor , Depar men of Compu er and Information Science, Universit y of Pennsylvania,Philadelphia, United States, 1995. [2] E.A. Boi t en, H.A. Par tsch, D. Tuijnman, and N.Völker; “How t o Produce Correct Soft ware – An In t roduc t ion t o Formal Specifica tion and Program Development by Transformat ions”. The Computer Journal, Vol. 35, No. 6, pp.547 – 554, December 1992.Pedro Rossel, Ricardo Contreras, María Cecilia BastarricaRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 200422[3] J.P. Bowen and M.G. Hinchey; “Seven MoreMyths of Formal Met hods”. IEEE Soft ware, Vol. 12, No. 4, pp. 34 – 40, July 1995.[4] I.M. Bradley; “Notes on Algebraic Specifications”.Information and Sof ware Technology, Vol. 31, No. 7, pp. 357 – 365, September 1989. [5] L.M.F. Carneiro, D.D. Cowan, and C.J.P. Lucena;“Introducing ADVchart s: a Visual Formalism for Describing Abs t rac t Da ta Views”. Technicalreport, Compu t er Science Depar t amen t & Computer Systems Group, University of Waterloo, Waterloo, Canada, 1993.[6] H. Ehrig, B. Mahr, I. Classen, and F. Orejas; “Introduction t o Algebraic Spe cification. Part 1: Formal Methods for Software Development”. The Computer Journal, Vol. 35, No. 5, pp. 460 – 467,October 1992.[7] H. Ehrig, B. Mahr, and F. Orejas; “Introduction toAlgebraic Specifica ion. Par 2: From Classical View t o Foundat ions of System Specificat ions”. The Comput er Journal, Vol. 35, No.5, pp. 468 – 477, October 1992.[8] K. Finney; “Ma t hema t ical No t a tion in FormalSpecification. Too Difficult for the Masses?” IEEE Transactions on Soft ware Engineering, Vol. 22,No. 2, pp. 158 – 159, February 1996.[9] M.D. Fraser, K. Kumar, and V.K. Vaishnavi;“Strategies for Incorpora ting Formal Specifications in Sof t ware Developmen t”. Communications of the ACM, Vol. 37, No. 10, pp. 74 – 86, October 1994.[10] C. Ghezzi, M. Jazayeri, and D. Mandrioli;“Fundamentals of Sof tware Engineering”. Prentice-Hall International Editions, 1991.[11] T.L. Good and J. Brophy; “Con t emporaryEductional Psychology”. Addison Wesley, 5 edition, January 1995.[12] J.V. Guttag, J.J. Horning, S.J. Garland, K.D. Jones,A. Modet, and J.M. Wing; “Larch: Languages and Tools for Formal Specificat ion”. Springer-Verlag,1993.[13] A. Hall; “Seven Myths of Formal Methods”. IEEESoftware, Vol. 7, No. 5, pp. 11 – 19, Sept ember 1990. [14] D. Harel; “On Visual Formalisms”.Communications of the ACM”, Vol. 31, No. 5, pp. 514 – 530, September 1988.[15] J. B. Johns on; “The Conour Model of Block Structured Processes. SIGPLAN Not ices, Vol. 6, No. 2, pp. 55 – 82, 1971.[16] K. E. Kendall and J. E. Kendall; “System Analysisand Design”. Prentice Hall, 4 edition, 1999.[17] I. Lee and O. Sokolsky; “A Graphical Propert ySpecification Language”. In Proceedings of 2nd IEEE Workshop on High-Assurance Sys temsEngineering. IEEE Computer Society Press, 1997.[18] D. Neary and M. Woodward; “An Experiment t oCompare he Comprehensibili y of Tex ual and Visual Forms of Algebraic Specifications”. Journalof Visual Languages and Computing, Vol. 13, No. 2, pp. 149 – 175, April 2002.[19] R. S. Pressman; “Sof tware Engineering. APractitioners Approach”. McGraw-Hill, 5 edit ion,June 2000.[20] P.O. Rossel; “A Language for FormalRequirements Specifica t ion wi th a Graphic Representation”, (In Spanish). Master's thesis, Universidad de Concepción, Concepción, Chile, January 2000.[21] J. A. Senn; “Analysis and Design of Informat ionSystems”. McGraw-Hill, 2 edition, January 1989.[22] I. Sommerville; “Sof t ware Engineering”.Addison-Wesley Publishing Company, 6 edit ion,2000.[23] J. M. Wing; “A Specifier's Introduction to FormalMethods”. IEEE Computer, Vol. 23, No. 9, pp. 8 – 24, September 1990.[24] J. Woodcock and M. Loomes; “Sof twareEngineering Ma t hema t ics”. Addison -Wesley Publishing Company, 1989.[25] A. E. Woolfolk; “Educational Psychology”. Allyn& Bacon, 7 edition, 1998.APPENDIX: FORMAL SYNTAXThe formal synt ax of t he algebraic specificat ion has been defined in [20], and we summarize it here. Figs. 9, 10, and 11 show this definition.Graphic specification of abstract data typesRevista Facultad de Ingeniería, Chile Vol.12 Nº1, 200423Fig. 9.- Formal definition of algebraic specification syntax (a)Fig. 10.- Formal definition of algebraic specificationsyntax (b)Fig. 11.- Formal definition of algebraic specificationsyntax (c)。
