Guiding Specification and OO implementation of Data Types
Contents
1. theStack equals old theStack trailer theStack equals old theStack insertFront x belong to UnboundedStack methods pop and push respectively When a specific implementation of UnboundedStack is de fined it is necessary to explicitly describe the relation be tween the JMLObjectSequence theStack and the structure that is chosen to store the stack elements This relation is known as the abstraction function Figure 2 exemplifies the definition of this relation as in 2 Although we recognize the important role played by model based approaches in general we believe that these kind of specifications are difficult to a first grade student to un derstand and master They involve additional data types that she has to learn to use Moreover the definition of the appropriate abstraction mapping from concrete implemen tations to the specification can be rather difficult to obtain to most of our students 3 OUR APPROACH Java class public class UnboundedStackAsArrayList extends UnboundedStack protected ArrayList elems in theStack maps elems theList into theStack protected represents theStack lt abstractValue protected represents_redundantly theStack such_that forall int i 0 lt i amp i lt elems sizeQ elems get i theStack itemAt i protected pure model JMLObjectSequence abstractValueQ JMLObjectSequence ret new JMLObjectSequence2. i amp amp size old size 1 In method void pop the pre condition requires isEmpty and the post condition ensures size old size 1 In method int top the pre condition requires isEmpty In method boolean isEmpty the post condition ensures result lt gt size 0 We cannot find suitable post conditions to express and mon itor the property that says that popping a stack right after having pushed an integer leaves the stack unmodified The inclusion of a post condition in method push with the flavor of pop equals old clone would not work because pop is avoid method Unless we have methods that allow to inspect the whole structure of the data type elements with out modifying it for instance a method int element int i for inspecting the i th element of the stack we are not capable of writing complete monitorable post conditions These inspection methods are in general artificial and even against the nature of the type itself and hence they are not a solution to the problem This example shows that when ever a specification is implemented by a mutable type there are properties that can not be expressed as monitorable con tracts of the class Algebraic specification is another well known ap proach to the specification of software systems that supports specification at a higher level of abstraction Algebraic ap proaches can be divided into two classes model orient
3. Proceedings of TOOLS USA 9S conference IEEE Computer Society Press 1999 13 14 15 18 G Leavens K Rustan M Leino E Poll C Ruby and B Jacobs JML notations and tools supporting detailed design in java In OOPSLA 00 Companion pages 105 106 ACM Press 2000 B Meyer Object Oriented Software Construction Prentice Hall PTR second edition 1997 I Nunes A Lopes V Vasconcelos J Abreu and L Reis Testing implementations of algebraic specifications with design by contract tools DI FCUL TR 05 22 DI FCUL 2005 J Spivey The Z Notation A Reference Manual International Series in Computer Science Prentice Hall 1992 The Joint Task Force on Computing Curricula Computing curricula 2001 final report Available at http www acm org sigcse cc2001 V Vasconcelos I Nunes and A Lopes From abstract data types to contract annotated java interfaces Lecture Notes http labmol di fc ul pt congu 2006
4. required to be defined in the domains section using expressions of the form op X Y if For instance pop S if not isEmpty S 5 Write the axioms e Prepare one axiom for each pair observer constructor Exceptions are the pairs ruled out by domain con ditions For each constructor c S T S and each observer o S U V use an axiom whose left hand side is of the form o c X Y Z where X has sort S Y has sort T and Z has sort U Example pop push S E S e For each derived operation d S T U or predi cate d S T write an axiom whose left hand side is of the form d X Y Example isEmpty S if size S 0 e Add the axioms that pertain directly to sort equal ity For example in a specification for rational numbers one may want an axiom of the form F G if num F den G num G den F e Prepare the axioms that relate constructors For example for sets we can have add add A X Y add add A Y 6 Did not succeed in writing the axioms Perhaps you need a different classification in step 3 or even a dif ferent choice of operations in step 2 Specification Analyzer The Specification Analyzer tool verifies the syntactic and se mantic correctness of a specification module A specification must conform to rules related to the signatures domains axioms and external names of the specification as follows Signatures are such that e The first parameter of a signatur
5. Guiding Specification and OO implementation of Data Types Isabel Nunes Faculty of Sciences University of Lisbon Portugal in di fc ul pt ABSTRACT Design by contract DBC is among the most popular tech niques that are taught in introductory programming courses aiming at helping students to learn how to construct correct and robust software Although we recognize the important role played by formal design as supported by DBC tech niques we have experienced for several years the frustration of not being able to guide students in writing contracts both that fully specify all the relevant properties and are moni torable The fact that students are left with very poor spec ifications leads them to perceive contracts as unnecessary and even irrelevant discouraging the further application of DBC We addressed these problems through the adoption of property driven algebraic specifications for the descrip tion of the observable behavior of programs Our approach comprises a tool assisted refinement process that supports the run time checking of implementations against specifica tions In this paper we present the approach and report on our experience of using it Keywords Algebraic specification implementation checking design by contract 1 INTRODUCTION Teaching object oriented software development at the Uni versity of Lisbon comprises a three semester programme ac cording to the objects first approach of the AC
6. Iterator iter elems iterator while Citer hasNextQ ret ret insertBack iter next return ret Q F Figure 2 Partial view of an implementation of UnboundedStack Contrasting with the above property driven specifications 6 can be very simple and concise for certain classes of types in particular for Abstract Data Types ADTs In this case the observable behavior of a program is specified simply in terms of a set of abstract properties The simplicity and ex pressive power of property driven specifications on the one hand and the necessity for students to test their classes against specifications on the other hand led us to the de velopment of a framework for creating and testing property driven specifications against implementations In this framework students proceed as follows 1 Build algebraic specifications structured as a specifi cation module to abstractly specify their data types 2 Input the specifications to a Specification Analyzer to obtain feedback on syntax and type correctness 3 Build Java interfaces from the above specifications si multaneously write a refinement mapping that relates i each interface with the sort it implements and iz each interface method with the specification operation it implements 4 Input the specifications the refinement mapping and the interfaces to a Refinement Mapping Analyzer to obtain feedback on their co
7. M Computer Science Computing Curricula 17 where students learn ba sic skills of OO programming specification analysis and design which they will further use in other courses of their BsC The first course gives students early exposure to the concept of object and class client and supplier while in troducing more traditional control structures The second course covers algorithms and fundamental data structures while the third focus on software engineering topics includ ing OO development using design patterns Vasco Vasconcelos Faculty of Sciences University of Lisbon Portugal vv di fc ul pt Antonia Lopes Faculty of Sciences University of Lisbon Portugal mal di fc ul pt This programme is based on the methodology of design by contract DBC in the sense that students are taught to built responsible client and supplier classes client classes invoke methods only when their pre conditions are met and supplier classes provide results according to method post conditions Difficulties arise in the use of the design by contract method ology namely with i contract extension in inheriting classes ii increase of class coupling when writing contracts for meth ods in presence of clientship transitivity and iii writing fully monitorable contracts that express all the desirable prop erties We identified and proposed solutions for the first two problems f9 10 The third one was identified in the evaluation of t
8. chnique that helped them to find bugs in their implementations but soon they realized that many of the important properties of their types were impossible to express through monitorable assertions The idea underlying the approach we developed which en compasses automatic generation of contracts was to gather the possibility of building meaningful and complete specifi cations with the capacity of checking implementations Using the approach described in this paper students are able to monitor all the axioms in their specifications One of the remaining problems has to do with some difficulties students now face in interpreting the feedback obtained by monitoring the contracts since this is given in terms of con tracts that they do not see and that they would scarcely understand even if they did Students must interpret con tract violations in the context of properties they have defined through algebraic specifications Further work addresses this difficulty by trying to present contracts in such a way that is on the one hand under standable to students and on the other closely related to the original specification that they wrote Acknowledgments Thanks are due to Jos Luiz Fiadeiro Joao Abreu and Luis Reis for insightful discussions 5 REFERENCES 1 The java modeling language examples page http www cs iastate edu leavens JML exam ples shtml 2 E Astesiano H J Kreowski and B Krieg Brckner ed
9. e g clients must be able to test pre conditions It is important that students test their classes in particular against contract violations To be monitorable a contract cannot have side effects thus it cannot invoke methods that modify the state These restrictions bring severe limitations to the kind of properties we can express directly through contracts Un less we define a number of otherwise dispensable additional methods we are left with very poor specifications that dis courage the further application of DBC Furthermore as argued by Barnett and Schulte 3 contract specifications do not allow the level of abstraction to vary and do not sup port the specification of components independently of the implementation language and its data structures Java class public class ArrayStack implements Cloneable public void clear public void push int i public int top public int size public boolean isEmpty Figure 1 Java implementation of an integer stack As an example let us analyze the support given by DBC to the specification of an integer stack through the integration of assertions in the class ArrayStack in Figure I Following Meyer 14 and using Java and JML rather than Eiffel this could be achieved by adding the following assertions In method void clear the post condition ensures size 0 In method void push int i the post condition ensures top
10. e must have the sort under specification the main sort e The result of any constructor operation must have the main sort therefore a predicate cannot be a constructor Domains are of the form Bigs 8 a if O where f is an operation not predicate 71 variables and is a formula Mn are Axioms must have one of the following four basic struc tures f ti irn t if 1 Diixsersty Y Q 2 not p ti tnr if 3 T 22 if 4 where f is an operation p is a predicate t is a term x is a variable and is a formula In either case the condition if is optional The following restrictions apply to these four structures e In if f is a constructor than t must be either a variable or a constructor applied to variables the remaining arguments t2 to tn must all be variables e In ip and if f or p are observers than t must be a constructor applied to variables e In i and if f or p are derived than all its arguments t to tn must be variables e In 4 z and x2 must be variables of the main sort External Names Any external name be it a sort which is not the main sort be it an operation that is not defined in the signatures part of the specification must be specified by some of the imported specification in the same module Refinement Mappings For each specification in a module we choose a Java type in terface or primitive for its representation In this proces
11. ed Users are given feedback that identifies the kind of violation pre or post condition All details including the architectural model and the rules for contract generation are described elsewhere 15 4 EXPERIENCE AND CONCLUSIONS In 2002 we reported on our experience with the contract based objects first approach encompassing three semesters 13 Here we concentrate on the second course Algorithms and Data Structures The approach described in this paper has been refined over the years Students are exposed to specifications to all the data structures studied in the course 18 They also de fine less common data structures in their course work such as a Video Disk essentially a bonded capacity index data structure whose elements are of distinct sizes The introduction of the guidelines for building specifications Section 3 represented a major leap in the students abil ity to prepare meaningful and complete specifications Stu dents not only have a method to attack the problem but they are also confident that they did not forget any axiom This confidence is reinforced by the possibility of checking the coherence of their specification using the Specification Analyser tool This strongly contrasts with what used to happen before when students were taught to write contracts first using iContract and later JML Students were initially very receptive to the idea of contract monitoring as a te
12. ed and property driven specifications Model oriented approaches to specification like the ones fol lowed by users of Z 16 Larch 8 JML and AsmL 3 definitely prevail within the OO community In most of these approaches the behavior of a class is specified through a very abstract implementation based on primitive but not necessarily basic elements available in the adopted speci fication language Implementations can be tested against specifications by means of runtime assertion checking tools but this requires that an abstraction function be explicitly provided In JML for instance a concrete implementation is expected to include JML code defining the relation be tween concrete and abstract states For example the abstract class UnboundedStack a model based specification of stacks taken from the JML distribu tion i relies on sequences more concretely on objects of type JMLObjectSequence a class belonging to the distri bution of JML The following two annotations are part of UnboundedStack abstract class public model JMLObjectSequence theStack public initially theStack null amp amp theStack isEmpty The JMLObjectSequence class defines immutable sequences including a series of methods for sequence manipulation from which the methods trailer insertFront that are used in this specification are examples The model un derlying JMLObjectSequence is a finite sequence of elements The post conditions
13. he aforementioned three semester course 12 This paper presents our approach to surpassing this prob lem which arises when students start writing and imple menting specifications of abstract data types The rest of the paper is organized as follows Section describes the problems that arise when adopting a design by contract approach to data type specification and imple mentation It also describes the use of model based alge braic approaches to specification and points its limitations within the context of a second semester course Section describes the framework we developed for writing imple menting and checking property driven specifications and that we currently apply in the second course Section reports on our experience in using the framework It also describes benefits and limitations of our approach as well as topics that need further work 2 MOTIVATION When following the design by contract methodology we experienced the frustration of not being able to guide stu dents in writing contracts both that fully specify all the relevant properties and that at the same time are moni torable Contracts are built from boolean assertions thus any method invoked within an assertion must return a value Further more contracts should refer only to the public features of the class because client classes must be able not only to un derstand contracts but also to invoke operations that are referred to in them
14. herence 5 Build classes that implement the above interfaces 6 Input the specifications the classes and the refinement mapping to a Contract Generator that automatically wraps the provided classes so that when executed the behavior of each class is checked against the cor responding specification Through the rest of this section we briefly describe signifi cant details about each of the above steps Specifications and Modules The specification language is to some extent similar to many existing specification languages In general terms it supports the description of partial specifications with con ditional axioms It has however some specific features including the classification of operations in different cate gories and strong restrictions on the form of the axioms Figures 3 and 4 present two examples specification import IntegerSpec sort IntStack constructors clear IntStack gt IntStack push IntStack Integer gt IntStack observers top IntStack gt Integer pop IntStack gt IntStack size IntStack gt Integer derived isEmpty IntStack domains s IntStack top s pop s if not isEmpty s axioms s IntStack i Integer top push _ i i pop push s _ s size clear _ zero _ size push _ s suc size s isEmpty s if size s zero _ not isEmpty s if not size s zero _ Figure 3 Specification of integer stacks specification sort Integer constr
15. implementation while the second is the name of the interface Examples in clude IntFraction and ArrayStack 2 Choose the representation the class s attributes write a body for all the methods in the interface 3 Write one or more Java constructors For each one pick a constructor in the specification and make sure that the Java constructor leaves the object as pre scribed by the post condition of the chosen specifica tion constructor For example an obvious choice for a stack Java constructor is to pick the method clear and write public ArrayStack clear Checking Classes Against Specifications The behavior of classes can be tested against the specifica tions they are supposed to implement by using the Contract Generator tool When given a specification module a re finement mapping and the classes that are to be tested the tool creates e An immutable version of each original class these classes are equipped with contracts that result from automatically translating the domains and axioms of the corresponding specifications e A wrapper class for each original class such wrap pers redirect every method call to the original class via the corresponding method in the immutable class Whenever a class client to the original classes is executed within the context of the tool every call to a method m in any of those classes is monitored that is pre and post conditions of m are evaluat
16. itors Algebraic Foundations of Systems Specification IFIP State of the Art Reports Springer 1999 3 M Barnett and W Schulte Spying on components A runtime verification technique In Proceedings Workshop on Specification and Verification of Component Based Systems OOPSLA 2001 4 M Bidoit and P Mosses CASI User Manual Number 2900 in LNCS Springer 2004 5 Contract based system development http labmol di fc ul pt congu 6 H Ehrig and G Mahr editors Fundamentals of Algebraic Specification 1 Equations and Initial Semantics Springer 1985 7 J Goguen J Thatcher and E Wagner An initial algebra approach to the specification correctness and implementation of abstract data types In Current Trends in Programming Methodology volume IV Data Structuring pages 80 149 Prentice Hall 1978 8 J Guttag J Horning S Garland K Jones A Modet and J Wing Larch Languages and Tools for Formal Specification Springer 1993 9 I Nunes Design by contract using meta assertions Journal of Object Technology 1 3 37 56 2002 10 I Nunes Method redefinition ensuring alternative behaviours Information Processing Letters 92 6 279 285 2004 11 I Nunes and V Vasconcelos Contract guided system development 2002 Presented at the ECOOP 02 Sixth Workshop on Pedagogies and Tools for Learning Object Oriented Concepts 12 R Kramer iContract The Java Design by Contract Tool In
17. r pred x Integer Integer lt _ x Integer x Integer IntStackSpec is type ArrayStack clear s IntStack Stack is void clear push s IntStack i Integer IntStack is void pushCint i pop s IntStack IntStack is void pop top s IntStack Integer is int top size s IntStack Integer is int size isEmpty s IntStack is boolean isEmpty O Figure 5 An example of a refinement mapping Notice that a refinement mapping may define a mapping from two different components into the same type interface or primitive This is extremely useful since it promotes the writing of generic specifications that can be reused in different situations as illustrated in reference 15 Refinement Mapping Analyzer The Refinement Mapping Analyzer tool verifies the syntactic and semantic coherence of a specification module a refine ment mapping R and a set of interfaces Mappings are subject to some constrains e Predicates must be bound to methods of type boolean e Only sorts defined in closed specifications can be bound to primitive types e Every n l ary operation or predicate f s 1 5n must be bound to an n ary method m ti tn such that t is the type that according to R implements sort si Implementing the Interfaces For building classes that implement the interfaces students must follow the following guidelines 1 Name your class A good choice is a compound name where the first part describes the
18. redicates can be expressed through axioms which in our case are closed formule of first order logic re stricted to some specific forms 15 Essentially we have axioms i that relate constructors ii that define the result of observers on constructors iii that describe derived op erations predicates results on generic instances of the sort and iv that pertain to sort equality Notice that because operations may be interpreted by par tial functions a term may not have a value The equality symbol used in the axioms represents strong equality that is to say either both sides are defined and are equal or both sides are undefined Specifications may declare under the import section refer ences to other specifications and may use external symbols i e sorts operations and predicates that are not locally declared For instance the specification of integer stacks imports IntegerSpec and uses sort Integer and operation symbols zero and suc which are external symbols Notice that the specification of integers in Figure 4 s self contained since it does not contains any external symbol We call it a closed specification The meaning of external symbols is only fixed when the specification is embedded as a component in a module A module is simply a surjective function from a set N of names to a set of specifications such that for every spec ification i the referenced specification names belong to N and ii
19. s we build a refinement mapping R between the module and the collection of Java types This mapping also describes the correspondence between the operations and predicates in the specifications and the methods in the interfaces Fur thermore for specifications that are mapped into primitive types the mapping defines how operations and predicates are expressed in terms of built in Java operations Only closed specifications can be implemented by primitive types An admissible refinement mapping for the IntegerStack module is presented in Figure It says that specification IntStackSpec is mapped into type ArrayStack whereas the sort Integer is implemented by the Java primitive type int The following are the guidelines given to students to build refinement mappings For each class involved ArrayStack in Figure 5 1 Choose the nature of the interface Will it describe imperative mutable objects or immutable objects Does pushing a value into a stack yields a new stack or on the contrary changes the state of the target object 2 Provide a mapping for each operation in the specifi cation Ignore the first parameter in each operation When the resulting sort of an operation is the sort under refinement choose between an immutable or an imperative method For example choose between Stack push and void push refinement mapping IntegerSpec is primitive int zero x Integer Integer suc x Integer Intege
20. the external symbols are provided by the cor responding specifications in the module The set N defines the set of components of the module For instance by nam ing the two specifications presented in Figures 3 and 4 as IntStackSpec and IntegerSpec respectively we obtain a module IntegerStack Students are provided with the following guidelines for build ing specifications 18 1 Identify your sort Below let it be S 2 Identify the operations and predicates and define their signatures The first parameter of each signature should be S 3 Classify the operations according to the three cate gories e Start with the constructors Candidates are op erations with signatures of the form op S S Do we need them all For each of them check whether it produces an intrinsically new value of sort S If the resulting value can be obtained oth erwise then the operation is not a constructor e Move to the observers Candidates are all the remaining operations and predicates Does each of them allow to observe a different facet of the values of the sort Or can you obtain one of them by using the remaining operators e The remaining operations are derived 4 Check the domain of each operation Are there oper ations that are not defined in the whole extension of its domain Are there particular values that make no sense as parameters to the operation Record the situ ations for which the operation is
21. uctors zero Integer gt Integer suc Integer gt Integer pred Integer gt Integer observers lt _ Integer Integer axioms 1 j Integer zero _ lt suc zero _ pred zero _ lt zero _ pred i lt j if i lt j suc i lt suc j if i lt j pred i lt pred j if i lt j pred suc 1 1 suc pred i 1 Figure 4 Specification of integers A specification defines exactly one sort the main sort and the first argument of every operation and predicate in the specification must have that sort Furthermore opera tions are classified as constructors observers or derived These categories comprise respectively the operations with which all values of the type can be obtained the operations that provide fundamental information about the values of the type and the operations where the provided information can be obtained through the remainder operations Predi cates can only be classified as either observers or derived Specifications are partial because operation symbols declared with can be interpreted by partial functions In the sec tion domains we describe the conditions under which inter pretations of these operations are required to be defined For instance in the specification of integer stacks both top and pop are declared as partial operations They are however required to be defined for all non empty stacks As usual in property driven specifications properties of op erations and p
Download Pdf Manuals
Related Search