Second-Order Principles in Specification Languages for Object
Contents
1. which range over the universe of a Kripke structure then the reflexive transitive closure of this relation is expressed by TC z 9 2 or more succinctly TC Strict transitive closure is denoted TC This represents the transitive closure of as opposed to the reflexive transitive closure of The restriction FO TC is such that only two variables x and y may appear in a formula For example the formula dy TC z yRal y x y A p y expresses there is a path of a edges from x to a vertex where p holds Reachability Logic RL is a fragment of FO TC with an unbounded number of boolean variables in addition to the two domain variables x and y 3 Boolean variables are first order variables restricted to range over 0 and 1 Formulae of the logic are constructed using an adjacency formula 6 z b y 6 which is a binary relation between two n tuples a b1 0n 1 and y b 0 _ This is in fact a disjunction of conjunctions where each conjunction contains at least one of the following x y Ra x y or Ra y x for some binary relation Ra Hence the adjacency formula necessarily implies that there is an edge from x to y or an edge from y to x or that x is equal to y Conjuncts may also contain expressions of the form b bj b 0 or b 1 For RL the formulae NEXT 6 denoting Ay 6 w 0 y 1 ly 2 REACH 6 i e 3y TC8 5 a 0 y 1 A dly a and CYCLE 6 i e T2. editor Handbook of Graph Gram mars and Computing by Graph Transformations World Scientific 1997 A Dawar and Y Gurevich Fixed point logics In The Bulletin of Symbolic Logic volume 8 pages 65 88 Association for Symbolic Logic 2002 M Fowler and K Scott UML Distilled 2nd ed Addison Wesley 2000 D Harel Dynamic logic In D Gabbay and F Guenthner editors Handbook of Philosophical Logic volume II chapter 10 pages 497 604 Reidel 1984 N Immerman Languages that capture complexity classes SIAM Journal of Computing 16 4 760 778 1987 D Jackson Automating first order relational logic In Foundations of Software Engineering pages 130 139 2000 D Jackson I Schechter and I Shlyakhter Alcoa the Alloy constraint analyzer In Proceedings ICSE 2000 pages 730 733 IEEE 2000 Klasse Objecten OCL center 1999 At http www klasse nl oc1 D Kozen and J Tiuryn Logics of programs In J van Leeuwen editor Handbook of Theoretical Computer Science volume B chapter 14 The MIT Press 1990 S Kreutzer Expressive equivalence of least and inflationary fixed point logic In Proceedings Symposium on Logic in Computer Science LICS IEEE 2000 S Kreutzer Pure and Applied Fixed Point Logics PhD thesis Aachen University of Technology 2002 G T Leavens A L Baker and C Ruby Preliminary design of JML A behavioral interface specification language for Java Technical report Iowa State Univ 2000 Ava
3. such as select project and join The select operator selects tuples from a relation whose attributes meet the selection criteria which is normally expressed as a predicate The project operator selects certain attributes from a single relation discarding the rest The join operator composes two relations Relational algebra forms the basis of a multitude of relational query languages these are used in order to manipulate the data of a relational database We discuss aspects of one of the standard languages SQL in Section 4 Examples of properties expressible in FOL are reflexivity and transitivity concatenation is an expressible composition We say that R is reflexive if Vx Rx and R is transitive if VaVyVz Ry yRz zRz The concatenation of two relations R and S is expressible by Ro S x z dy zRy A ySz Note that we use the notation xRy for x y R and R x y respectively On the other hand properties that demand the finiteness of certain sets of elements are not expressible For example all elements are at most related to a finite number of other elements Furthermore many properties that demand the existence of a finite but unknown number of elements which are related in a cer tain way are not expressible For example quantifications such as Jn 3x1 n which are routinely used in mathematical notation do not exist in FOL and often cannot be expressed by any other means Another typical
4. Having spawned a much larger community of users and tool developers who are now actively in volved in its development JML has since become the standard specification language used for verification of Java programs JML is used to specify Java classes and interfaces 23 24 The Spec system 5 has been developed as a specification language for Net The recent developments in the JML community have been influenced and some ideas have been adopted that originated from the Spec project The treatment of second order concepts is similar in both languages we concentrate on JML in the following Specifications in JML are formulated by making use of side effect free boolean Java expressions they are written as Java comments The original JML tool is a pre compiler designed to translate specified programs into Java pro grams that explicitly monitor assertions at run time Specification violations that are found throw Java exceptions Since JML s conception many more tools have been developed using JML as an input specification language For a more extensive overview of JML tools and applications see 8 When specifying transitive closure JML manages to avoid the whole issue of acyclicity by defining recursive datagroups 28 These have been designed primarily with frame condition issues in mind To solve the information hiding problem i e that protected or private fields of a class should remain hidden from their clients the represents
5. but important example is transitive closure The transitive closure of a relation R is the relation TC R such that for all elements x and y the relation TC R x y holds if and only if there is a finite number of intermediate points 20 2n where n N with x zo y Zn and zi 1 Rz for 1 lt i lt n Accordingly one cannot express in FOL that some point b is R reachable from some other point a i e TC R a b An alternative yet equivalent definition of transitive closure TC R is 1 TC R is transitive 2 R C TC R and 3 if R is transitive and R C R then TC R C R The latter condition is not expressible in FOL as it implicitly quantifies over R It is important to note however that the transitive closure of a structure can be expressed in a FOL setting if the structure is both finite and acyclic see Section 4 3 Extensions of FOL In this section we investigate a number of extensions of first order logic including transitive closure logic fixed point logic and first order dynamic logic These extensions allow us to express various properties and compositions of relations that cannot be expressed using first order logic alone Transitive Closure Logic First order logic extended by a transitive closure operator written FO TC and called transitive closure logic was first in troduced by Immerman 16 If we let the formula represent a binary relation on two n tuples of domain variables
6. clause was introduced to JML allowing one to specify the representation of concrete fields by particular abstract fields Hence protected or private fields in an implementation can be changed without changing the specification visible to its clients Unfortunately the use of abstract fields generated problems with the modifies clause A method s modifies clause specifies those locations that are permitted to be changed by execution of the method This was fixed by a depends clause which relates those locations used to determine an abstract location s values A datagroup can be modelled by an abstract location whose value contains no information By using a depends clause a location can be declared to be in a datagroup therefore membership in a datagroup allows the locations in the datagroup to be modified whenever the datagroup is mentioned in the modifies clause The license to modify a datagroup implies the license to modify the members of the datagroup as defined by a downward closure rule 25 For any set of datagroups S the downward closure of this set is the smallest superset of S such that for any group G in the closure of S all nested datagroup members of G also belong in the closure of S For example consider the following Java linked list with Node objects having next and value fields class Node Integer value Node next The datagroups nodeValues and nodeLinksare are defined recursively using clauses such as maps next n
7. of data types Technical Report XI MIT Labo ratory for Computer Science 1974
8. C 6 d a 0 x 0 are also formulae of RL Hence it is possible to describe in this logic steps out of the current vertex x paths out of x and cycles from back to itself Importantly the boolean variables allow Propositional Dynamic Logic PDL and the variation of Computational Tree Logic CTL to be embedded in RL Consider the PDL formula a p which is a true property of a state s whenever there is some state t in which p holds that is reachable from s by execution of a The regular expression can be translated into an non deterministic finite au tomaton Na with n states Within the framework of RL the adjacency formula of a is a translation of the transition relation of Na whereby each state of the automaton is represented by k 1 log n bits with 0 and I representing the initial and final states respectively For example if a is the sequential composi tion 7o m then a transition from state s to state t in Nro n is represented by the adjacency formula Rro y Ab1 b s V Ry x y A b b t where b by is the initial state and bj b is the final state Hence an example of a formula in RL is REACH 6 p where 4 a bi be y bf 05 is Rag x y A b1b2 00 A bib 01 V Ra x y A bib2 01 A b1 b3 11 This has the meaning that it is possible to take the path of a mo edge followed by a 71 edge to a point where p holds this is just ro 71 p in PDL Regular Expressions Over Relations Kle
9. P of a relation R a formula with two free variables is said to be expressible if there is a closed formula p R such that for all models M the interpretation RM has property P if and only if p R is true in M Here R is the single interpretation of relation R in M The formula p R must be effectively constructible from any given R in a uniform way This notion is extended to properties of tuples of relations Formally a property is a relation on relations A composition C of relations R R is expressible if there is a formula wp R1 Re a y with free variables x and y such that wp R1 Rx is the relation composed from RM RM Here wp Ri Rx is the single interpretation of Yp R Rg x y in M The formula wp Ri Rk must be effectively constructible from any given R Rp in a uniform way Formally a composition is a function on relations Note that the constructibility of and w neither implies the decidability of P nor respectively the computability of C This is because the validity of the constructed formula is in general undecidable Moreover the composition of relations may be iterated but the properties themselves cannot be iterated Relational algebra is a formal system used for manipulating relations The set of its operations may vary per definition but it usually includes set operations since relations are sets of tuples and special operators defined for relations
10. Second Order Principles in Specification Languages for Object Oriented Programs Bernhard Beckert and Kerry Trentelman 1 Department of Computer Science University of Koblenz Landau beckert uni koblenz de Automated Reasoning Group Australian National University Kerry Trentelman anu edu au Abstract Within the setting of object oriented program specification and verification pointers and object references can be considered as re lations between the elements of a data structure When we specify prop erties of these data structures we often describe properties of relations Hence it is important to be able to talk about relations and their proper ties when specifying object oriented programs or programs with pointers Many interesting properties of relations such as transitive closure finite ness and generatedness are not expressible in first order logic FOL hence neither are they expressible in first order fragments of specifica tion languages In this paper we give an overview of the different ways such properties can be expressed in various logics with a particular em phasis on extensions of FOL i e transitive closure logic fixed point logic and first order dynamic logic Within the paper we also discuss which of these extensions already are or in fact should be implemented within specification languages We feel that such a discussion is necessary since it is often the case that when an extension of FOL is implemen
11. ct the formulae such that they are positive in the relation variable R This leads us to the definition of least fixed point logic Least Fixed Point Logic Least Fixed Point Logic LFP is the extension of FOL by the following rule if R is a k ary free relation variable z is a k tuple of free first order variables f is a k tuple of terms and y R z is a formula in which R oc curs only positively then lfp p y t is also a formula For any structure A that provides an interpretation of the free variables of y except for Z A H lfp p29 t if and only if the interpretation of t in A is in the least fixed point of the operator defined by y R Z Consider for example the directed graph V where V is a set of n vertices and E C V x V is a set of ordered pairs i e edges Then the transitive closure of E is defined as ifp r z y Ey V 3z Rz A zRy 2 y Inflationary Fixed Point Logic Inflationary Fixed Point Logic IFP can be con sidered the simplest non monotone fixed point logic It is the extension of first order logic by the following rule if R is a k ary free relation variable z is a k tuple of free first order variables t is a k tuple of terms and y R Z is a formula then ifp r zp t is also a formula Let A be a structure which pro vides an interpretation of the free variables of y except for z The operator I R a a Ror A R v is inflationary and therefore has an infla tionary fixed point R Henc
12. e AF ifpr zy t if and only if the interpreta tion of in A is in the inflationary fixed point An interesting result is that both least and inflationary fixed point logics are equally expressive on arbitrary structures 21 First Order Dynamic Logic The principle of dynamic logic DL is to fa cilitate the formulation of statements about program behaviour by integrating programs and formulas within a single language see e g 15 20 for general ex positions of DL By permitting arbitrary programs a as actions of a labelled multi modal logic dynamic logic provides formulas of the form a and a When considering states during program execution as worlds of modal logic a expresses that all terminating executions of program a lead to states in which holds whereas a is a true property of a state s whenever there is some state t reachable from s by execution of program a in which holds A Hoare style specification a w of partial correctness can be expressed as gt a w In contrast to Hoare logic and temporal logic approaches to program verifica tion dynamic logic permits the expression of structural relationships between different programs by using multiple modalities For example relative correctness statements like a a as well as nesting are possible as in the formula lal c gt 0 gt a e lt d d Provided that they are computable dynamic logic can express properties of relation
13. endency graph whereby 1 each table R is a node 2 there is a directed arc from R to Rj if R is defined in terms of Rj and 3 the arc is labelled if the query defining R is non monotone with respect to Rj i e by adding something to Rj we may cause something to be removed from R The maximum number of arcs on any path from R in the dependency graph is called the stratum of node R A recursive query statement is said to be stratified if every node has a finite stratum i e there are no cycles containing arcs Hence legal SQL3 recursive queries are required to be stratified Note that this technique can also be used in other languages using fixed point definitions in order to exclude non monotonicity cases that lead to fixed points being undefined CASL The Common Algebraic Specification Language CASL has been de veloped by CoFI the international Common Framework Initiative for algebraic specification and development see website at http www cofi info The al gebraic approach to software specification was conceived in the early 1970s see for example 35 Programs are considered as algebras consisting of datatypes and operations the intended behaviour of a program is specified by formulae involving these operations The development of dozens of languages all with slight variations in syntax and semantics demanded the need for a common framework hence CoFI was formed The resulting specification language CASL featur
14. ene algebras are algebraic struc tures that generalise the operations of regular expressions A Kleene algebra consists of a set K with binary and operations a unary operation and constants 0 and 1 In general the algebra s operational semantics depends on the model but typically involves some notion of finite iteration A Kleene algebra gives rise to a relational algebra extended with reflexive transitive closure when the following interpretations of the operations are made operation as join el ement 0 as the null empty relation element 1 as the identity relation and as the reflexive transitive closure of a relation As mentioned previously an extension of first order logic with the ability to write list next or even more generally to be able to use regular expressions to describe terms or term sets would be very useful There exist approaches which allow an extended syntax for terms in first order logic For example in 10 recursive term definitions are added to first order logic Rather than using regular expressions and Kleene algebras to extend FOL it is possible to manipulate FOL formulae such that they fulfill a purpose similar to that of regular expressions Two ways to define words and or formal languages are by using 1 predicate logics such that each model corresponds to a word in the language and 2 modal logics such that each path in a Kripke structure corresponds to a word There is a large amount
15. ers are available in a specification language it is possible to define transitive closure and other properties of rela tions in the language Otherwise this is possible only for finite relations which is mostly adequate In our opinion the best solution is that which is taken by CASL and JML namely by building freeness or minimal fixed points either ex plicitly or implicitly into the language It still seems desirable to add regular expressions to specification languages It is not clear yet how this should be done this is the subject of future work References 1 W Ahrendt T Baar B Beckert R Bubel M Giese R H hnle W Menzel W Mostowski A Roth S Schlager and P H Schmitt The KeY tool Software and System Modeling 4 32 54 2005 2 N Alechina S Demri and M de Rijke A modal perspective on path constraints Journal of Logic and Computation 13 1 18 2003 3 N Alechina and N Immerman Reachability logic An efficient fragment of tran sitive closure logic Logic Journal of the IGPL 8 3 325 337 2000 4 T Baar The definition of transitive closure with OCL Limitations and appli cations In Proceedings of the Fifth Andrei Ershov International Conference on Perspectives of System Informatics LNCS 2890 pages 358 365 Springer 2003 5 M Barnett K R M Leino and W Schulte The Spec programming system An overview In Construction and Analysis of Safe Secure and Interoperable Smart Devices Inte
16. es partial functions subsorts sort generation constraints first order logic and structural and architectural specifications 27 In CASL datatypes are specified using the keyword type and are given in terms of sorts i e the types of values and constructors Datatypes may be de clared to be either generated or free When a generated datatype is declared spec GENERATED_CONTAINER sort Elem generated type Container empty insert Elem Container pred is_in__ Elem x Container Ve e Elem C Container e e is_in empty ec is_in insert e C amp e e Ve is_in C end spec TRANSITIVE_CLOSURE sort Elem pred __R_ Elem x Elem free pred _Rt__ Elem x Elem Va y z Hlem exRy aRty exRtyAyRtz 2xRtz end Fig 2 CASL specifications then the corresponding sort is constrained to be generated only by the declared constructors For example in the specification of GENERATED CONTAINER taken from the CASL User Manual 7 see Figure 2 the generatedness con straint is such that any value of sort Container is denoted by a term built only with operators empty insert and variables of sort Elem Note that within this specification the pairs of underscores _ indicate place holders for the binary predicate is_in and the bulleted list features ax ioms which constrain the predicate Essentially the generatedness constraint allows one to prove by induction on the declared constructors properties o
17. f values of the sort Container A free datatype declaration has the same inter pretation as the generated datatype declaration with the additional property that all distinct constructor terms of the same sort denote distinct values In CASL a freeness constraint using the keyword free can be im posed on a predicate declaration This has the effect that a predicate that is consistent with the given axioms but not a consequence of the axioms will be false predicates hold minimally We can see this in the specification of TRAN SITIVE_CLOSURE shown in Figure 2 also taken from 7 Here the transitive closure of a binary relation R on some sort Elem is specified Since predicates hold minimally in models of free specifications Rt is actually the smallest tran sitive relation including R OCL The Object Constraint Language OCL 19 is a part of the Unified Modeling Language UML 14 Currently the industry standard UML allows software developers to graphically specify visualise and document models of soft ware systems OCL can be used to augment UML object models with additional textual information which cannot otherwise be expressed by UML diagrams This additional information takes the form of side effect free expressions and constraints An expression is a specification of a value A constraint is a restric tion of one or more values in part of the object oriented model The semantics of OCL constraints is defined by an eva
18. g A A a fixed point P of F is any set P C A such that F P P A fixed point Q is called the least greatest fixed point of F if and only if Q C P P C Q holds for all fixed points P of F The function F is said to be monotone if F X C F Y for all X C Y C A A well known theorem by Knaster and Tarski states that every monotone function has a least and a greatest fixed point 33 For limit ordi nals and the monotone function F consider the sequence X aeora of sets X CA defined by i X Q ii Xe F X and iii X User XS A fixed point X is reached in this sequence whereby X X for the least ordinal a such that X X This fixed point X is called the inductive fixed point of F A second theorem by Knaster and Tarski states that the least and inductive fixed points coincide hence any least fixed point of a monotone function can be defined inductively by a sequence of sets as described above Dually the greatest fixed point of a monotone function F can be defined induc tively using the sequence X acora of sets X C A defined by i X A ii X 1 F X and iii X Neer XS Note that if F is inflationary i e X C F X for all X C A rather than monotone then X is called the inflationary fixed point of F Next let 7 be a signature t e a finite set of relation symbols and let A be a structure consisting of a universe A and interpretations for each relation symbol in r Consider a firs
19. ilable at ftp ftp cs iastate edu pub techreports TR98 06 TR ps gz G T Leavens E Poll C Clifton Y Cheon C Ruby D Cok and J Kiniry JML reference manual At http www cs iastate edu leavens JML jmlrefman K R M Leino Specifying the modification of extended state Technical Report 1997 026 Digital Systems Research Center 1997 L Mandel and M V Cengarle On the expressive power of OCL In Proceedings FM 1999 LNCS 1708 pages 854 874 Springer 1999 P D Mosses CASL A guided tour of its design 1999 Available at http www brics dk Projects CoFI Documents CASL GuidedTour index html1 P M ller A Poetzsch Heffter and G Leavens Modular specification of frame properties in JML Technical Report 02 02 Iowa State University 1997 Object Management Group UML resource page 1999 At http www uml org J Rumbaugh Relations as semantic constructs in an object oriented language In Proceedings OOPSLA 1987 pages 466 481 1987 A Schtirr Adding graph transformation concepts to UML s constraint language OCL In Proceedings First Workshop on Language Descriptions Tools and Ap plications LDTA ENTCS 44 Elsevier 2001 JCC s SQL std page At http www jcc com SQLPages jccs_sql htm A Tarski A lattice theoretical fixpoint theorem and its applications Pacific Journal of Mathematics 5 285 309 1955 J Yang SQL3 recursion Lecture notes Stanford University 1999 S Zilles Algebraic specification
20. in OCL This coding makes use of the OCL iterate construct which iterates through all items of a collection verifying a given con dition and possibly updating the value of a variable returned at the end of the iteration The algorithm itself calculates the transitive closure of a directed graph V where V is a set of n vertices and E C V x V is a set of ordered pairs i e edges A path from vertex vp to vg is denoted vp gt vg and is a se quence of edges vo v1 U1 v2 Uk 1 Uz The intuition behind Warshall s algorithm is this if the graph contains paths v gt w and w u whose interme diate vertices belong to the set S then the graph also contain a path v gt u such that the intermediate vertices belong to S U w The algorithm iterates from 1 to n At the k iteration it selects paths whose intermediate vertices come from v1 Ur 1 Unfortunately the resulting OCL code of this algorithm is about one and a half pages in length it is neither intuitive nor easy to read and furthermore it requires the directed graph to be finite A transitive closure construct for OCL is proposed by Schiirr in 31 This is based on features of the path expression sublanguage similar to OCL of PROGRES a graph transformation language The transitive closure operator is implemented to keep track of already visited objects and therefore avoids any cyclic problems Schiirr defines it as follows self ancestors self a
21. luation function which maps in a given object diagram any constraint to one of the logical constants true false and undefined Admissible diagrams are those whereby all constraints of the corresponding class diagram evaluate to true The type of an OCL expression is either pre defined Boolean Integer etc or it is the type of a class in the corresponding class diagram Dot notation is used for accessing the attributes of objects The basic data structures of OCL are the collections Set Bag and Sequence OCL does not have a primitive operator for transitive closure but it does al low recursion Consider the following OCL invariant in the context Person where ancestors are recursively defined in order to represent the transitive closure of the relation defined by parents note that both ancestors and parents are of type Set Person ancestors parents gt union parents ancestors The expression parents ancestors computes the set of all ancestors of a set of parents and returns a value of type Set Person Now suppose A is a parent of B who in turn is a parent of C Then the minimal object structure which solves the constraint is such that the parent of B is A and the ancestors of C include both B and A However additional solutions involve situations where B and A are both ancestors of each other and themselves In our case we would prefer to use the minimal solution corresponding to the minimal fixpoint but this cannot alwa
22. ncestorsClosure self self ancestorsClosure visited0bj let S self ancestors gt excludeAll visited0bj in S gt collect ancestorsClosure S gt union visited0bj gt asSet This definition will suffer from the unclear semantics of the let construct As mentioned in Section 2 it is possible to define the transitive closure of relations known to be finite and acyclic To illustrate this Baar 4 de fines ancestors by APar x Par x U y dz z Par x Ay APar z where Par x and APar x are the translations of x parents and x ancestors respectively Correspondingly in first order logic this definition can be expressed by the formula r z y r a y V dz r x z Ar z y where the relation symbols r and r are substituted for Par and APar with r x y meaning y Par x and r x y meaning y APar x This formula is interpreted by the structure U R R where U is a universe of variables and R and R are interpretations of the relations r and r respectively Countermodels for this formula are presented whereby R does not coincide with the transitive closure of R However if the model U R R is finite and the axiom 7r x x holds enforcing R s acyclicity then R is a correct definition of transitive closure however in general finiteness is not expressible JML and SPEC The Java Modeling Language JML was originally de signed by Leavens et al at Iowa State University in 1998
23. odeValues into nodeValues Hence the clause modifies list nodeLinks when it is added to the JML specification of a method sortInPlace Node list says that all node objects reachable from list may be changed whenever sortInPlace is executed Such specifications rely on a smallest fixed point semantics for recursive defi nitions built into JML Gleaned from mailing list discussions Leavens et al have considered introducing regular expressions i e writing list next in order to specify the JMLObjectSet of all objects reachable from list using the field name next but have rejected this as not particularly beneficial since using datagroups seems to be an adequate enough solution 5 Conclusions Although important properties of relations are not expressible in classical first order logic it is possible to extend first order logic e g with fixed point and transitive closure operators in order to describe such properties We find that all specification languages feature modifications which allow them to extend beyond the limitations of first order logic For example SQL implements fixed point logic OCL uses the iterate and let constructs CASL implements the notion of freeness whereas JML incorporates built in recursion However the logical concepts underpinning these modifications are often not well documented This paper has attempted to clarify what is going on regarding these extensions Generally we have found that once integ
24. of literature on the latter For 1 we fix a family of signatures X4 They contain the binary relation symbol lt a constant symbol first a unary postfix function 1 and for every a in the alphabet A we have the unary relation symbol Qa The set of words over A is denoted A For w A A where A is the empty word the associated X 4 structure is denoted M the empty model is not possible The formula Mw Qa first holds true if and only if the first letter of w is a The formula Mw H Qs 1 holds true if and only if the second letter of w is b etc For 2 we express information about semi structured data represented as a graph by imposing constraints on the possible paths through the graph Such a constraint might be all objects reachable by a path p are also reachable via a path q where p and q are sequences of labels possibly involving regular expressions In order to check that the constraints hold we re cast them as model or satisfiability checking tasks in some logic usually modal For example see 2 where this is done using propositional dynamic logic and 12 where this is done using monadic second order logic Fixed Point Logic Fixed point logics are particularly well suited for mod elling recursion and have consequently found applications in various areas of computer science such as database theory finite model theory and formal veri fication Following 22 13 for a set A and a function F
25. ogic the Object Constraint Language OCL uses the iterate and let constructs the Common Algebraic Specification Lan guage CASL uses the notion of freeness and the Java Modeling Language JML incorporates built in recursion However it is often the case that the modifica tions made to specification languages are done in a make do fashion and their designers are unaware of the logic underpinning their decisions In this paper we attempt to clarify what is really going on within these specification languages Our work is carried out in the framework of the KeY project The KeY system is a commercial CASE tool augmented with specification and deductive verifi cation functionalities 1 see website at www key project org KeY uses the Unified Modeling Language UML for visual modelling of designs and specifica tions along with OCL for specifying constraints and other expressions attached to the models 29 The target language for program verification is Java Both the specification language OCL and the verification language of the KeY tool namely dynamic logic have second order elements as described in Section 4 Our case study experience has shown that often there is a need for expressing second order principles in a more usable and or flexible way this need provides the motivation behind our investigations In particular a modifies clause has been recently implemented within the KeY system 6 As the above example demonstrates i
26. rnational Workshop CASSIS 2004 Marseille France Revised Selected Papers LNCS 3362 Springer 2005 6 B Beckert and P H Schmitt Program verification using change information In Proceedings SEFM 2003 pages 91 99 IEEE Press 2003 7 M Bidoit and P Mosses CASL User Manual Introduction to Using the Common Algebraic Specification Language LNCS 2900 Springer 2004 8 L Burdy Y Cheon D Cok M Ernst J Kiniry G Leavens K Leino and E Poll An overview of JML tools and applications In Formal Methods for Industrial Critical Systems FMICS 2003 volume 80 of ENTCS Elsevier 2003 9 M V Cengarle and A Knapp A formal semantics for OCL 1 4 In Proceedings The Unified Modeling Language UML 2001 LNCS 2185 Springer 2001 10 H Chen J Hsiang and H Kong On finite representation of infinite sequences of terms In Proceedings of 2nd International Workshop on Conditional and Typed Rewriting Systems number 516 in LNCS pages 100 114 Springer 1990 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 3l 32 33 34 35 S Cook A Kleppe R Mitchell B Rumpe J Warmer and A Wills The Amsterdam manifesto on OCL 1999 Available at http www trireme com whitepapers design components 0CL_manifesto PDF B Courcelle The expression of graph properties and graph transformations in monadic second order logic In G Rozenberg
27. rs SQL3 supports linear recursion a recursive query has the form WITH RECURSIVE R AS r Q where r is the expression that you want to recurse and R is its name that can then be used in the associated query expression Q If we consider a query as a function on tables then a recursive query computes the fixed point table 34 Essentially we start with R as an empty table We then evaluate r using the temporary contents of R and replace R with this new value As long as R R we continue to evaluate r and replace R by its new value Once R R we compute Q using the current contents of R and output the result The example shown in Figure 1 outlines how we find Mary s ancestors from the schema ParentChild parent child The first part of the recursive definition utilising is the base case Its meaning is that all parent child pairs are also ancestor descendant pairs Although initially we know nothing about ancestor descendant relationships after the first round we deduce that parents are ancestors and children are descendants In each subsequent round we use the facts deduced in previous rounds to get more ancestor descendant relationships We eventually stop when no new facts can be proven When the query Q is non monotone i e adding tuples to R might cause some tuple to be removed from the result of Q then the fixed point iteration may not converge A way to circumvent this is to construct a dep
28. s that are ordinarily not expressible in pure first order logic For example to express that y is reachable from x via applications of the function nezt i e x and y are related in the transitive closure of the relation p defined by p u v iff v next w can be expressed by while x 4 y x next x true 4 Specification Languages In this section we look at the approaches that specification languages take in defining transitive closure and similar properties of relations Most require hacks to force a model s finiteness and acyclicity before transitive closure can be determined an interesting and unique approach is taken by the Java Model ing Language JML Alloy The Alloy Analyzer implements an automatic analysis method for formu lae of relational logic 17 18 This logic acts as an intermediate language for the object modelling notation Alloy It is a first order logic with sets and relations whereby each formula is accompanied by a declaration that associates variables to their types The combination of formula and declaration is called a problem There are three kinds of types set relation and function Scalar variables are treated as singleton sets and sets are encoded as degenerate relations For ex ample a scalar variable v of set type T can also be represented as the relational type T Unit where Unit is a special type designed for this purpose A navigation expression s r denotes the image of a set s
29. t order formula y R Z with R a k ary free relation symbol not occurring in 7 and 7 a k tuple of free variables On A the formula y induces a fixed point operator Fy e A gt e A such that F R a A R H v Here A R a means that formula y is satisfied by the interpretation that assigns to each variable x of z the element a of ae AF Below we investigate three fundamental fixed point logics monotone least and inflationary fixed point logics First of all we discuss monotone fixed point logic Using this logic we can nest inductive definitions from one fixed point built up from a formula we can define another Monotone Fixed Point Logic Monotone Fixed Point Logic MFP is the extension of FOL by the following rule if R is a k ary free relation variable z is a k tuple of free first order variables t is a k tuple of terms and y R Z is a formula such that the corresponding operator Fy is monotone on all structures then lfp r z t is also a formula For any structure A that provides an interpretation of the free variables of y except for 7 A H lfp g zp E if and only if the interpretation of in A is in the least fixed point of the operator defined by y R Z As we have mentioned previously the least and greatest fixed point of any monotone operator always exists However it is undecidable as to whether a formula induces a monotone operator In order to guarantee monotonicity on the operator one can restri
30. t would be advantageous to be able to express transitive closure in OCL in an easier fashion than the current method which is by using the OCL iterate construct described in Section 4 The paper is organised as follows in Section 2 we look at how one goes about expressing properties of relations and composing relations We discuss various properties which may or may not be expressed in first order logic This logic s lack of expressiveness leads us to an examination of a number of extensions of first order logic in Section 3 In Section 4 we discuss several specification languages and the approaches they take in determining properties of relations Finally we draw conclusions in Section 5 2 Relations and Relational Formulae in a FOL Setting We are interested in both expressing properties of relations and composing rela tions in relational formulae In this section we provide the basic definitions for these notions and briefly discuss relational algebra We conclude by describing a number of properties which can or cannot be expressed in first order logic How ever before we begin we need to stipulate what we mean by a relation within an object oriented language Following 30 we say that a relation expresses the symmetric form of those associations which are represented in a programming language as pointers or object references Hence we model both object references and pointers as first order functions on objects A property
31. ted within a specification language it is done so in an ad hoc manner or the under pinning logical concepts are not well documented 1 Introduction When it comes to specifying object oriented programs we need to be able to a refer to a set of particular objects in an object structure and b talk about the properties of the relation between the objects As an example consider the definition of sets of related objects which are used in modifies clauses a modifies clause allows one to specify those parts of a program state that are exclusively allowed to change 28 6 To illustrate suppose we have a linked list with objects of class Node having a next field For a method say sortInPlace it would be useful to be able to write list next in the method s modifies clause where denotes some form of transitive closure Its semantic intention would then be that the set of locations that are reachable from list using the field next may be modified during the method s execution One may also wish to specify that the list is not cyclic assuming that this is the case a field such as position may be introduced such that it returns a reference to a node at a given position If the position is less than or greater than 1 then the field returns null All specification languages have some form of modification which allows them to extend beyond the limitations of first order logic For example the query lan guage SQL implements fixed point l
32. under a relation r The encoding of sets as degenerate relations allows a uniform syntax to be given to such expressions i e if p is a person then p mother will denote p s mother whereas p parents will denote the set of p s parents A transitive closure opera tor is also included in Alloy For example the formula p N Jd 0 expresses that p is acyclic Here Id is the identity relation and 0 is the empty relation Because relational logic is undecidable it is in general impossible to prove that a formula is either consistent or valid To determine for a given formula whether a model exists within a particular scope the Alloy Analyzer places restrictions on the size of the sets of the basic types A model is said to be within a scope of k if it assigns to each type a set consisting of no more than k elements SQL In order to manipulate the data of a relational database relational query languages based on relational algebra are used The database query language SQL was adopted as an industry standard in 1986 32 Having undergone two major revisions SQL3 is now the current version WITH RECURSIVE AncestorDescendant ancestor descendant AS SELECT FROM ParentChild UNION SELECT adi ancestor ad2 descendant FROM AncestorDescendant adi AncestorDescendant ad2 WHERE adi descendant ad2 ancestor SELECT ancestor FROM AncestorDescendant WHERE descendant Mary Fig 1 SQL specification Unlike its predecesso
33. ys be found there may be more than one equiva lent solution or it may not even exist A suggestion to uniquely characterise the minimal solution is given in 11 This paper suggests mimicking induction over a natural number n This is exhibited in the following OCL specification ancestors up_to n if n 1 then parents else parents gt union parents ancestors_up_to n 1 Nat gt forall ancestors_up_to n ancestors_up_to n 1 implies ancestors ancestors_up to n Of course this makes the assumption that the models are finite Alternatively as done in 9 we can use the OCL let construct to stipulate that the inheritance relationship must be acyclic Note that self refers to any instance of the class in which it is specified let parents self parents let ancestors self parents gt union self parents ancestors in lt some_expression_using_definition_of ancestor gt The let construct is a new addition to OCL introduced in version 2 0 The expression let x e in eg evaluates expression e gt with each occurrence of x replaced by the value of e1 Its use avoids evaluating the same expression multiple times However the construct s semantics within OCL is not entirely clear 9 Whether arbitrary recursively defined expressions are allowed is uncertain Thus using let to define transitive closure is not advised In 26 the transitive closure of a relation is computed by coding the well known Warshall s algorithm
Download Pdf Manuals
Related Search