Home

Biblioteca Digital

1. 3 2 A Complete Calculus Useful for Alloy Users 3 2 1 Proper Point Dense Omega Closure Fork Algebras 3 2 2 Translating From Alloy to PDOCFA 3 2 3 Interpretability of Alloy in PDOCFA Dynamite 4 ha ae ln xoxo Red ROAD RACER RO Og 4 1 Implementation remarks 4 1 1 Embedding the Alloy Calculus in PVS 4 1 2 Overview of Dynamite s Architecture 4 2 Features of Dynamite s 4 2 1 Introduction of Hypotheses and Lemmas 4 2 2 Introduction of cases 2 22222 llle 4 2 3 Hiding sequent formulas 4 24 Pruning of goals llle 4 2 5 Automated Witness Generation iEvaluati M o cig hee Oe bun do Bode MA abel ec Eun nod wes Eg 5 1 Evaluating Dynamite as a plain prover for Alloy 5 1 1 Case Study Addressing for Interoperating Networks 5 1 2 Evaluation le eae De aad ens Res 5 2 Evaluating characteristic features of Dynamite 5 2 1 A Running Example Binding in Network Domains 5 22 Pruning of goals sls 5 2 3 Automated Witness Generation 5 2 4 Using the Alloy Analyzer as a Proof Helper viii 6 Discussion Limitations amp Conclusions 0 04 90 List of Symbols and Conventions lll 98 Appendix 100 A Complete Proofs of Lemmas from Chapter3 101 B Case Study Proof of Mo
2. fact UnarySumOperandOlsNotUniv all t UnarySum t operandO in UnivSyntax run witnessSearch some t UnaryTerm some t unaryValue and all v t unaryValue a v Fig 4 11 Fragment of Alloy model with internalized Alloy syntax 4 Dynamite 71 Validating a Witness Precandidate lines 8 9 A witness precandidate t is valid in an environment In contrast a witness candidate must be valid in all environments In order to analyze whether t can be considered as a witness candidate we modify the Alloy model from Fig 4 10 by replacing assert existentialAssert by the following assert witnessPrecandidateValidation some t and all v t o v The assertion requires t to denote a nonempty set in which all the ele ments satisfy formula alpha in all environments If no counterexamples are produced by the Alloy Analyzer term t is stored in the algorithm output variable result and promoted to witness candidate Witness Precandidate Failure by Over Approximation lines 13 20 Let us assume that witness precandidate t fails in environment According to Section 4 2 5 this implies that either t is empty in or some value from the set denoted by term t does not satisfy a The second condition may hold even if t provides at least one value that satisfies in each environment In this case we say that term t over approrimates a witness candidate In order to avoid this over approximation we will use two techn
3. aori e FB E a andi c B e a if and only if i either i 8 or not i ie v gt E e i eee 0 Ea wheni FQ Ea otherwise int Val cal n i let 72 22 a Ai E 3 Formal background 26 ie Ui tm e Ea iE plei en iff where p is the predicate declared as pred p zi e1 zx ex o ib a1 an iff Pee and when n gt 1 iE a2 an for all relation R C me E univ i ie v o R E v ind amp amp R v d gt a exist a relation R C ro E univ i such that ie vo R E vind amp amp R v d amp amp a do not exist a relation R me E univ i s t i v o R E v ind amp amp R v d amp amp a exist at most a relation R ro E univ i s t ip v o R E v ind amp amp R v d amp amp a exist exactly one relation R C ES E univ i s t ig v o R E v ind amp amp R v d amp amp a oe Ealv d iff e E some v d iff cs Enov dla iff e lone v d iff EN Eonev d iff e quant n d all na nm d f where quant is all some no lone or one quant bind all bindz bind f where quant is all some no lone or one es quant ni ma d f iff c E H quant bindi binds f iff Where d is the result of removing multiplicity keywords from d if any and v d is the re
4. p T t p T v by Def t p v by Def T a v a v by Def 3 2 5 a a a a t by set theory and Def t if v ranges over higher order relations p T t p T v by Def t p v by Def T a1 a2 ay a1 02 ag alu by Def 3 2 5 a1 a2 xak a1 02 0k a t by set theory and Def t e if t t t2 Since both the result of the lemma and the definition of e are given by cases we will consider 6 different cases depending on k the rank of t1 and ka the rank of t2 Following the typing constraints of Alloy navigation is not defined when ky ka 1 101 A Complete Proofs of Lemmas from Chapter 3 102 k 1 and k2 2 then k 1 p T t p T 6 12 by Def t p T t1 e T t2 by Def T p ran T t1 T t2 by Def e ran p T t p T t2 by p homomorphism ran a a a a ti a b a b as t2 y by Ind Hyp ran a 0 a a ti a b a t2 by De b b Ja a a ti a b alta by Def i b b b a ti a t2 by Def b b b a t t3 by a homomorphism bb bea t by Def t Notice that p T t1 p T t2 a a a a t b1 bg gu 01 b2 bx alta by Ind Hyp 1 b1 b2 x x bka b1 a t4 b1 ba m bka a t2 i by Def Then ran p T amp p T
5. e AX pa e Xx e pa Xy e p er e2 Xx e1 p Xa eo p er amp ez Xa 1 pay amp Xa e2 py 1 2 Xx e1 pa Xa eo p e1 Vez Xx ex pa V Xa e2 px let v e1 ez Xx e2 pk o v gt e1 L L i L memes EOQEOW U iai iu on vk Xx e py otherwise a gt e else ez XxX e p ifa is true on px Xx e2 py otherwise Tab 3 3 Meaning of Z PDOCFA expressions Note that the operation symbols in the right column represent the operations of Def 3 2 1 with the exception of representing relational override and gt representing a maping DEFINITION 3 2 4 Satisfiability of PDOCFA formulas We will say that a PDOCFA formula a in the context of a language L L Z PDOCFA is satisfiable w r t a proper PDOCFA 2 and an instance ph denoted by A ph a according to the following statements PDOCFA 3 Formal background 34 A pa fe 21 e2 iff Xx e1 px Xa 2 px Li 1 Li A pa oora if not 9L px Proc rum a raum sn 3 pa Poca I B y a ES poco OT 2 pa B A ud nora amp amp B i 2L pa PR and 2 px Spo 2 ES Poors 77 B iff mot 2 Pa noc or 9I Pat IPDOCPA 9L px bx 9 B if A pa bo if and only if 9L pa mun EJE 2 L I NEN E 9L pa Folt v e o iff A px SA e Xy e pa Tae A p H let v a iff a is EU oc yendo od z PDOCFA A pa a otherwise PDOCFA A p H 8 when A p E o L E gt poe PDOCFA
6. BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 CCCCcb conAuthPurse c conAuthPurse amp amp XiConPurse cb c cb conAuthPurse amp amp c ether in cb ether amp amp cb archive c archive Rule prop Applying propositional simplification B Case Study Proof of Mondex Property 112 this yields 3 subgoals Rbc init 1 1 1 Concrete c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 cb conAuthPurse c conAuthPurse Rule assert Simplifying rewriting and recording with decision procedures This completes the proof of Rbc_init 1 1 Rbc_init 1 2 1 Concrete c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 XiConPurse cb c cb conAuthPurse Rule hide all but 1 4 3 Keeping 1 4 3 and hiding this simplifies to Rbc init 1 2 1 c conAuthPurse cb conAuthPurse 2 XiConPurse c cb c conAuthPurse 1 XiConPurse cb c cb conAuthPurse Rule replace 1 hide
7. Fig 5 8 Predicate stating the reachability of an identifier in a domain assert BindingPreservesReachability all d d Domain newBinding ldentifier Identifier IdentifiersUnused d newBinding ldentifier and AddBinding d d newBinding implies all i Identifier g Agent ReachablelnDomain d i g implies ReachablelnDomain d i g pred IdentifiersUnused d Domain2 new Identifier no d routing Agent amp new and no d dstBinding Identifier amp new and no Identifier d dstBinding amp new Fig 5 9 A nontrivial assertion BindingPreservesReachability bound identifiers are not used in d This latter condition is formalized by the predicate IdentifiersUnused A domain is called deterministic if each identifier is associated to at most one agent Assertion BindingPreservesDeterminism states that whenever a new binding for an unused identifier is added to a deterministic domain it remains deterministic A domain is considered non looping if the transitive closure of the bind ings for that domain has no cycles Assertion BindingPreservesNonlooping then states that the addition of a new binding to a non looping domain keeps this condition as long as the transitive closure of the new binding does not have cycles Another desirable property of a network is the capability to send a mes sage to the sender of a previously received message This is called return ability A domain in which it is
8. PDOCFA Aa mee A UTD l A pL a otherwise A pi A pi al vila iff for all relation R Ra A p O v gt R boxe some v a iff exists some relation R Ra A p O v gt R E EQ PDOCFA PDOCFA We will say that a proper PDOCFA 2 satisfies a PDOCFA formula a from the language L denoted by A E a if there is a relational instance ba for XA such that A ph E 12 PDOCFA 3 2 2 Translating From Alloy to Z PDOCFA The first step of the translation process starting from an Alloy specification S will be to build a language L Z PDOCFA where every Alloy constant defined by the user in S has its PDOCFA counterpart in L We will say that the language L and the Alloy specification S are compatible when their constants can be correlated in this way Although the languages in 4PDOCFA share most of the operations with Alloy at least intentionally and notationally there are remarkable differ ences such as a while the relations defined in Alloy can have arbitrary arity using PDOCFA only binary relations can be manipulated b PDOCFA offers the fork operator which is not directly tied to any Alloy operator c PDOCFA bears the request for point density d at least apparently PDOCFA lacks support for bounded integers and e while quantification in Alloy ranges over atomic elements from signatures in PDOCFA quanti fiers range over all the relations in the domain In the next sections we will show how
9. amp newBinding 1 Identifier 4 AddBinding d 1 d 1 newBinding 1 1 all i Identifier g Agent ReachableInDomain d 1 i g gt Reac ShableInDomain d 1 i gl Rule ff U pvs DH P UU G E A SESE Fig 4 2 Screenshots of Dynamite at one of the first sequents of a proof a without pretty printing and b with pretty printing 4 Dynamite 57 inRange_fint n int bool min_fint lt n and n lt max_fint e this PVS theory includes the definition of a subtype of int called fint that represents the Alloy integers in the interval fint TYPE n int inRange fint n e all the integer operations supported in Alloy addition subtraction multiplication integer division and remainder are modeled as PVS functions on fint For example addition is defined as add fint ni n2 fint fint IF inRange fint ni n2 THEN n1 n2 ELSIF ni n2 gt max fint THEN min fint 1 ni n2 max fint ELSE max fint ni n2 min fint 1 ENDIF As discussed at the end of section 3 2 2 it must be noted that this theory does not support models in which the set of integer atoms is not finite 4 1 2 Overview of Dynamite s Architecture The current prototype of the Dynamite Proving System was developed as an extension of PVS Therefore we wrote Emacs extensions for system commands such as those for opening and editing an Alloy specification Lisp routines that interact with the PVS prover
10. ether in cb ether 1 some b ConWorld Rbc b cl amp amp BetwInitState b Rule prop Applying propositional simplification this simplifies to Rbc init 1 1 Concrete c 1 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 some b ConWorld Rbc b c amp amp BetwInitState b 110 B Case Study Proof of Mondex Property 111 AT THIS POINT WE USE THE WITNESS CANDIDATE POSTULATION ROUTINE WHICH SUGGESTS cb AS THE WITNESS Rule inst 1 cb Instantiating the top quantifier in 1 with the terms cb this yields 2 subgoals Rbc init 1 7 1 Concretel c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 Rbc cb c amp amp BetwInitState cb Rule prop Applying propositional simplification this simplifies to Rbc init 1 1 Concrete c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 Rbc cb c Rule expand Rbc Expanding the definition of Rbc this simplifies to Rbc init 1 1 Concrete c 2
11. 12 bo Kees by b2 Kees bka 3 dbi bi a t4 b1 b2 RE bka a tz by Def ran bo X by D2 x x bka H ba goce bka a t a ta by Def bo x bka b2 x by A bo yet bka a ty t2 by a homo bak x bka b2 x bka D2 bx a t by Def t From the definitions of 7 and p we can reason s ran p T 1 p T t2 p bo b3 x lt x bka ba b3 T bka a t A 1 Joining the previous proofs we obtain p T t p T t1 t2 by Def T p T t1 e T t2 by Def T p r ran T t1 T t2 p by Def e r ran p T t1 p T t2 p by p homomorphism bo b3 x x bka b2 03 bx a t by A 1 A Complete Proofs of Lemmas from Chapter 3 103 k 2 and k2 1 then k 1 p T t p T t1 t2 by Def t p T t1 e T 13 by Def T p dom T t4 T t2 by Def e dom p T t1 p T t2 by p homomorphism dom a b a b a t1 b b b alta by Ind Hyp dom a b a b a ti b alta y by Def a a 3b a b a ti bE a te by Def Dom a a a alt a ta by Def a a a alt ta by e homomorphism a a a a t by Def t k 2 and kz gt 1 p T t p T t1 t2 by Def t p T t1 e T t2 by Def T p T t T t2 by Def e p T t1 p T t2 by
12. Semanticsot TD euo rub buc I SERV eR AE ed 30 Em PDOCFAcexpressions cce son dene oh eR vie ce edes bre der 32 ph Relational instance for a PDOCFA language 0005 31 ILA Collection of relational instances 0 cece sese 31 X x Meaning of PDOCFA expressions ssssssssse eee 32 pres Satisfiability of PDOCFA formulas eee 33 e PDOCFA operator for Alloy navigation seen 38 Xx PDOCFA operator for Alloy Cartesian product sess 38 T Tar Translation of Alloy terms 0 00 cece eect I 4T F Fy Translation of Alloy formulas ssseseee I 49 98 LIST OF FIGURES 2 1 a A signature declaration and b three different instances for it 2 2 Example of navigation between non binary relations 2 3 Proof rules of sequent calculus 3 1 Declaration of signature Dir llle 4 1 PVS embedding of the PDOCFA theorem corresponding to the Alloy assertion BindingPreservesReachability see Fig 5 9 4 2 Screenshots of Dynamite at one of the first sequents of a proof a without pretty printing and b with pretty printing 4 3 C amp C view of the Dynamite architecture les 4 4 Example of use of the rule dps hyp o 4 5 Strategy to transform the sequent T F a A intoT at A 4 6 Example of a sequent obtained after the application of several proof commands 2544 ad E uuu x ue ux aqu d s 4
13. T e2 univ T e1 lt T e2 e1 gt e2 T ei amp univ T e2 1 e2 dom T e1 dom T e2 lt T e1 T e2 er gt e T e1 T e2 T e1 T e2 if e1 is a function symbol eilez T e2 e T e1 otherwise a gt implies es else ez F a gt T ei else T ez let v1 1 Un En e let T v1 2 T e1 T vn T en T e Lv1 e1 Un tn a Ci where C is a fresh constant symbol and 7 is the count of comprehension expressions formerly seen Being n a positive numeric constant 0 ifn 0 m succ 0 ifn 1 succ succ 0 ifn 2 He card T e ne bw T ne e sum int e int T e ne add nes T nei bw T nea nei sub ne T ne1 bw T nez ne mul nes T ne1 w T nea ne div ne T ne1 bw T ne2 nei rem ne T nei Yow T ne2 sum 01 d1 Un d ne sum e T di T d Tab 3 4 Definition of mapping of Alloy terms to PDOCFA expressions 3 Formal background 49 Translation of Alloy formulas Once the translation of terms has been presented we introduce the transla tion from Alloy formulas to PDOCFA formulas The translation differs from the one presented in Frias et al 2004 in that the target of the translation is a first order language rather than an equational language and therefore it is no longer necessary to encode quantified variables because they are kept explicit This will greatly improve the readability of the translated formulas by Alloy
14. We can express the collection of objects contained in do along with the respective name of each one of them in do by using the composition operator in the following way d contents Composition of binary relations is well understood but for relations of higher arity the following definition for the composition of relations is considered R S a1 ai 1 A Jb a1 a 1 6 ER A b b2 Dj e being R and S relations of arity and j respectively Then the expression d contents denotes a binary relation where in every tuple can be found a directory contained in d and the name for which it can be referenced in d see Fig 2 2 In general Alloy terms are built from signatures signature fields and constants such as univ set of all objects in the model iden identity binary relation on the set univ and none the empty set Relational operators Notice that the phrase o is contained in d should not be read literally As mentioned above since both o and d are atoms they do not contain anything they are indivisible That phrase is intended to refer to the conceptual model being described by the Alloy specification Thus it should be read as the object represented by o is contained in the directory represented by d 2 Modeling and Analysis of Abstractions 10 are used to build more complex terms Difference union intersection and composition of relations are denoted by amp and respectiv
15. all a Z lsome b Z a b amp amp b lt succ a all a b Z Max a amp amp Min b gt succ a b Having defined the successor of a numeric point n defining its prede cessor noted prev n additive inverse pwn addition of numeric points n and m n py m subtraction n py m multiplication n bw m in teger division n pw m the remainder of the integer division n V6gy m and power n y becomes an easy exercise We present the definition of addition as an example ala Z la p0 a all a b Z a py succ b succ a pw b From now on when referring to these operations we will omit the subscript bw where possible to improve readability Once the operations have been defined we can axiomatize the proper value of the endpoints as well as remark that bw must be greater than 2 Min 25 1 Max 25 1 1 bw gt succ succ 0 Supporting the Alloy cardinality operator requires the addition of a new function card to PDOCFA As expected points have cardinality 1 The cardinality of an arbitrary relation is defined by formulas that for finite relations make card return the number of tuples all r Point r card r succ 0 Unary predicate Some characterizes nonempty relations e A retrieves a pair con tained in A and stands for set difference 3 Formal background 43 card 0 all r Some r card r succ 0 pw card r e r Since numeric constants
16. in order to lighten the workload of the task of proving 1 Introduction 5 Contributions The contributions of this thesis can then be summarized as follows e We present a complete proof calculus for the Alloy modeling language e We introduce an interactive theorem prover for Alloy assertions that extends the PVS theorem prover so that Alloy assertions can be proved using Alloy syntax This theorem prover called Dynamite was devel oped by us as part of the work of this thesis e We facilitate the interaction between PVS and the Alloy Analyzer in order to reduce the number of theorem proving errors induced by introduction of false lemmas hiding of necessary hypotheses or intro duction of erroneous hypotheses e We present a heuristic to reduce the proof search space based on the use of UnSAT cores to remove potentially unnecessary antecedents and consequents in a sequent The technique also allows us to remove formulas from the underlying theories being considered e We present a technique based on SAT for automatic generation of witness candidates for existentially quantified Alloy assertions e We present several examples including some complex case study Ra mananandro 2008 Zave 2005 2006 that allow us to assess the usefulness and usability of Dynamite These contributions have been presented in Frias et al 2007 Moscato et al 2010 2014 This document presents revised and augmented versions of the afo
17. Address implies i in d space and i in AddressPair implies i addr in d space and Postconditions d endpoints d endpoints and d space d space and d routing d routing and d dstBinding d dstBinding newBinding j Fig 5 7 Alloy predicate modeling the addition of a new binding newBinding to a domain d The variable d represents the resulting domain that contains newBinding and all the bindings from d if the new binding could be added to d according to the preconditions stated in the predicate A predicate AddBinding states how a domain is affected by the addition of new bindings Fig 5 7 In the context of this model an agent g is considered reachable in a domain d from an identifier if e iis connected to an address a in the reflexive transitive closure of the binary relation formed by all the bindings corresponding to d e a cannot be bound to another identifier in d and e in domain d a can route messages to g In Alloy reachability is modeled by the predicate shown in Fig 5 8 Figure 5 9 presents assertion BindingPreservesReachability This assertion states that if an agent is reachable in a domain d it is also reachable in the domain resulting from adding a new binding to d provided that the newly 5 Evaluation 82 pred ReachablelnDomain d Domain2 i Identifier g Agent some a Address a in i d dstBinding and a lin d dstBinding Identifier and g in a d routing
18. Alloy specification used as input of the translation Accordingly the resulting PVS specifications are also composed of two parts one for handling the log ical elements of PDOCFA theories and another for handling the extralogical ones Embedding of the Logical Aspects of a PDOCFA theory In the general part of the specification the following elements are defined e A data type called Carrier representing the set R of binary relations from Def 3 2 1 e Constants and functions representing the constants and operators from Def 3 2 1 See table 4 1 for a comprehensive list of the PVS elements representing each proper PDOCFA operator and constant e PVS axioms capturing the axioms and inference rules presented in Def 3 2 9 For instance RA 1 AXIOM FORALL x y z Carrier composition x composition y z composition composition x y z 52 4 Dynamite 53 duin PVS embedding sum x 0 x 1 Carrier Carrier amp product x 0 x 1 Carrier Carrier i complement x 0 Carrier Carrier 0 zero Carrier univ one Carrier composition x 0 x 1 Carrier Carrier iden one prime Carrier converse x 0 Carrier Carrier RTC x 0 Carrier Carrier Notice that the question mark is a valid character for an identifier in PVS Tab 4 1 Embedding of PDOCFA symbols and constants from Def 3 2 1 in PVS e Auxiliary constants operators and predicates as the ones presen
19. Analysis Jackson 2012 which provides numerous examples of varied complexity illustrating features of Alloy Nevertheless a formal description of the syntax and semantics of the language will be presented in the next chapter 2 1 1 Alloy terms and formulas As with every formal language Alloy can be studied from a syntactic or from a semantic point of view On the semantic side we will be working with relations of arbitrary but finite arity These relations which can be 2 Modeling and Analysis of Abstractions 7 ay Name no na a Name no a ay Name b Fig 2 1 a A signature declaration and b three different instances for it sig Name seen as sets of tuples of atomic elements will be the first order citizens of the language The gap between the syntactic domain and the semantic domain is bridged using instances also called environments Much the same as val uations from classical first order logic map variables to semantic values environments map Alloy expressions to relations Given an alloy model M we denote by am an instance for M Unary relations along with the atoms that they contain can be declared in Alloy by defining so called signatures For example the statement shown in Fig 2 1 a forces the existence of an unary relation Name holding all the atoms of type Name in the range of each instance applicable in the model M In fact the symbol Name can be used to deno
20. Rbc b c amp amp BetwlnitState b check Rbc_ init for 10 but 2 ConState 10007s check Rbc init for 10 but 10 ConState aborted by user after Th computation minisat According to the original model it took the Alloy Analyzer 2 8 hours to analyze the assertion using 2 ConState and the analysis was interrupted after 7 hours for a scope of 10 ConState We verified this assertion using Dynamite in under 10 minutes During the proof it was necessary to deter mine a witness for the existential quantifier in assertion Rbc init It took Dynamite 90 seconds to provide the correct witness The complete proof of the assertion may be seen in Appendix B Example 4 This example allows us to show a case in which Dynamite provides a non atomic coverage as witness candidate We present the Alloy model including assertion coverSample in Fig 5 10 Running the witness candidate generator on assertion coverSample returned the coverage i i2 Notice that term i i2 is not a solution due to fact f2 Let us consider the Alloy instance depicted in Fig 5 11 Notice first that the instance is indeed a model for the specification Also the instance shows that i2 alone cannot be a witness candidate If we permute i2 and i in Fig 5 11 we see that i cannot be a witness candidate It took Dynamite 16 seconds to provide the witness 5 2 4 Using the Alloy Analyzer as a Proof Helper Let us see the schematic representation of the proof tree fo
21. The axioms supporting the numeric part of the translation showed in the previous section The inference rules for the closure fork calculus are those for classical first order logic choose your favorite ones plus the following equational but infinitary proof rule for reflexive transitive closure given gt 0 by z we denote the relation inductively defined as follows x l x and zt E iden in y xin y xt in y u Rule F x in y 3 Formal background 46 The axioms and rules given above define a class of models Proper PDOCFA belong to this class but there might be models for the axioms that are not proper PDOCFA Fortunately the following theorem which follows from Frias et al 1997 Frias 2002 Thm 4 2 and Maddux 1991 Thm 52 states that if a model is not a proper PDOCFA then it is isomorphic to one THEOREM 3 2 10 Every PDOCFA 2 is isomorphic to a proper PDOCFA B Moreover there exist relations ap ag ai ai y possibly infinitely many of them that belong to 8 such that iden a5 00 42 5 05 05 3 22 While this theorem is important in itself since it implies that the calculus is complete with respect to the properties valid in proper PDOCFAs it is necessary in order to prove theorems on the appropriateness of the deductive mechanism we will provide for Alloy in Section 3 2 3 3 2 3 Interpretability of Alloy in PDOCFA One of the main goals of this thesis
22. Thesis TUM WEBER T 2008 Integrating a SAT Solver with an LCF style Theorem Prover in Proceedings of PDPAR 2005 ENTCS 144 2 pp 67 78 ZAVE P 2005 A Formal Model of Addressing for Interoperating Net works in Proceedings of the Thirteenth International Symposium of For mal Methods Europe Springer Verlag LNCS 3582 pages 318 333 2005 ZAVE P 2006 Compositional binding in network domains In Misra J Nipkow T Sekerinski E eds Proceedings of Formal Methods 2006 the 14th International FME Symposium Volume 4085 of Lecture Notes in Computer Science Hamilton Canada Springer Verlag 2006 332 347 LIST OF SYMBOLS AND CONVENTIONS Conventions Unless explicitly stated the following conventions are used in the whole document greek lowercase letters a 3 7 etc are used to represent logic formulas greek capital letters T A etc to represent sets of logic formulas latin italic lowercase e e e1 2 etc expressions latin italic capital r s and t R S T relations latin italic capital a b and c A B C sets latin italic capital L lan guages gothic capital letters A B etc PDOCFA structures latin italic lowercase v v U1 v2 etc variables latin italic lowercase c c c1 ca etc constants latin italic lowercase s s 1 9 etc Alloy signatures latin italic lowercase f f fi fo etc Alloy fields latin italic lowercase n n mi n etc Alloy numeric expres sions l
23. and available to the user to be used as lemmas to be proven later As we discussed in Chapter 1 the idea of mapping Alloy to an expressive enough formalism in which to carry proofs on is not entirely new It has already been done for instance with Prioni Arkoudas et al 2004 The 3 Formal background 47 essential advantage of the mapping we propose in this thesis is that the resulting formalism is extremely close to Alloy and therefore easier to grasp by standard Alloy users While this feature may be useless in the context of fully automated tools for which the language target of the translation may be ignored by the user it is of utter importance for user guided tools In fact our APDOCFAs are so close to Alloy that they allow us to only present Alloy formulas and expressions to the user during the whole proving process In the remaining parts of this section we give a proof of the interpretability theorem The main part of an interpretability theorem is a mapping from Alloy formulas to formulas in the language of PDOCFA The mapping is defined in two stages since Alloy terms must be mapped as well We will present maps T mapping terms and F mapping formulas As reader will see both mappings participate in each other s definition Comprehension expressions The comprehension expressions allow the user to define anonymous relations with specific restrictions imposed on its tuples We try to keep the target language a
24. automatic theorem prover for higher order logic Dynamite complements the partial automatic analysis offered by the Alloy Analyzer with semi automatic verification through theorem proving It also improves the theorem proving experience by using the Alloy Analyzer to provide au tomatic functionality intended for early detection of errors proof refinement and witness generation for existentially quantified properties Keywords Interactive Theorem Proving SAT Solving Alloy Calculus PVS Specification Analysis Agradecimientos Acknowledgments Gracias a todos Los que est n cerca los que est n lejos los que ya no est n Si hoy puedo estar escribiendo estas l neas es porque ustedes estuvieron ah Gracias a mis docentes a mis alumnos a mis compa eros a mis colegas a mis amigos Gracias por hacerme sentir que lo nico que separa esos grupos son las comas Tengo una dedicatoria que los nombra expl citamente a todos pero no me alcanza ni el margen ni la hoja Les prometo llevarla escrita en la mirada en cada abrazo que nos re na Thanks to Dr Natarajan Shankar Dr Daniel Jackson Dr Santiago Figueira and Dr Carlos Areces for giving me the honor of having them as the committee of this thesis Their questions advices and suggestions have resulted in a dramatic improvement in the quality of this document Gracias a mis queridos amigos que se vieron forzados a jugar de spar rings idiom ticos y tanto trabajo tuvieron
25. be seen as an instance builder Given an Alloy model and a scope specifica tion basically bounds for the sizes of the signatures the analyzer tries to automatically build some instance of such size in which all the facts of the model hold We will say that such instance is a legal instance of the model The whole search space denoted by the scope specification is exhaustively traversed so that if any instance can be build under the given settings the analyzer will do it In order to perform this task the Alloy Analyzer translates the model to a propositional formula The translation heavily depends on the bounds declared in the check command Once a propositional formula has been obtained the Alloy Analyzer employs off the shelf SAT solvers and in case a model of the formula is obtained it is translated back to an instance of the source model and presented to the user using different visualization algorithms Simulation Recall that in the previous section we exemplified how a flaw in a model can be detected by inspecting a specific instance The Alloy Analyzer allows the user to exercise this simulation strategy in order to iteratively improve the specification being developed The language itself provides particular purpose constructions to specify instance building requests and the bounds to be used on it For example the following statement specifies a search for an instance in which all the signatures may have at most three eleme
26. by the following axioms and proof rules 1 Axioms for Boolean algebras characterizing amp none and univ 3 Formal background 45 all x x x x allx x amp x x all x y x y y x allxy x amp y y amp x all x y z x y z x y z all x y z x amp y z 2 x amp y amp z all x y z x x amp y x all x y z x amp x y x all x y z x amp y z x amp y x amp y all x y z x y amp z x y amp x y all x x amp none none all x x univ univ all x x amp x none all x x x 2 univ Formulas defining composition of binary relations transposition re flexive transitive closure and the identity relation all x y x y z x y z all x x iden iden x x all x y z x y amp z none gt z y amp x none gt x z amp y none all x x iden x x all x y x y univ in y univ x y univ amp x y univ Formulas defining the operator V all x y xVy x T y p all x y xVy wVz x w y z TV p in iden formula enforcing point density all x x none amp amp x in iden gt some p Point p amp amp p in x Term univ univ Vuniv amp iden to be abbreviated as ideny defines a partial identity on the set of urelements Then the following formula forces the existence of a nonempty set of urelements univ ideny univ univ
27. calls required by the iterative technique Often during the original proof necessary formulas were incorrectly hid den We do not have precise records of the number of times this happened because those erroneous proof steps which at the time were not considered important were most times undone We only kept track of 9 cases where the reveal command was used in order to exhibit a previously hidden for mula but these were just a few of the cases It is worth comparing with the single case where the UnSAT core based technique missed a formula This missed formula is recovered if instead of using a scope of 3 in calls to the Alloy Analyzer scope 5 is used Recalling that we have proved 5 Alloy assertions the proofs of assertions BindingPreservesDeterminism and BindingPreservesNonLooping required fewer for mulas during the proof based on UnSAT cores This shows that the original proof used unnecessary formulas that were removed using rule dps hide A more qualitative analysis of the techniques allows us to conclude that refining sequents and theories using UnSAT cores leads to a shift in the way the user faces the proving process Looking at the usually few re maining formulas after dps hide is applied helped the user gain a better understanding on the property to be proved This feature was one of the most useful in the verification of the model developed by Zave 2006 The importance of this rule is that it provides a guide in the construct
28. contents A y y ob A a xy a ET by Def of 7 is z a d a some y Object d a xy in contents y y ob due to the relationship between contents and contents and ob and ob d a some y Object d a y in contents amp amp y ob because ob is an atom from Object d a da ob in contents It is worth emphasizing that while Alloy formulas and PDOCFA formulas are close there are still differences between the formalisms The differences from the Alloy language arise when we need to prove properties of e or X that require using the underlying fork algebra definition that includes the operator V We expect the number of properties involving the definition of such operators to be small compared to the complete proof For example in the case study we are reporting 25 out of 60 proved lemmas required dealing with the low level representation of e Yet 18 out of these 25 properties relate to properties of e that may be reused along other proofs For example among these 18 properties the following general properties are included all A set univ B set univ R set A gt B S set A gt B a A 3 Formal background 40 R in S implies a R in a S all A set univ B set univ R set A gt B S set A gt B R B S B R S B all A set univ B set univ C set univ W set A gt B gt C a A a W in B gt C We include a library with those properties of e and X that we conside
29. engine to implement the Dynamite specific commands the pretty printing of the formulas etc and Java code whose purpose is the translation and validation of formulas goals and specifications as well as the postulation of witness candidates for existentially quantified assertions among others A component and connector view diagram of Dynamite s architecture showing the interactions between the main components of the system is depicted in Fig 4 3 As explained by Owre 2008 the PVS prover engine runs as a subpro cess of Emacs through an ad hoc ILISP interface Kaufmann et al 2002 We added the implementation of the Dynamite specific commands to be Tt is worth noting that as usual in C amp C diagrams despite being of the same type not all the client server connectors showed in the figure are implemented in the same way For example the connectors between the Dynamite Translator and the Alloy Analyzer are implemented using the API exposed by the latter while the connectors linking the Dynamite proof commands processor and the Dynamite Translator are implemented through the OS standard input output subsystem 4 Dynamite 58 Alloy Mode p d Specification Translator m Dynamite Formula Goal Validator SSE system commands processor Expression Formula Translator gt Candidate Postulator gt User Dynamite proof a commands ALLOY Z processor PVS PVS Typechecker Prover DPS
30. example let us consider the Alloy modeling language Jackson et al 2001 Alloy is a formal specification language that allows one to create data domains and express properties of relations defined over those domains We will present Alloy in Section 2 1 but we point out here that Alloy is not decidable since it extends classical first order logic It even in cludes reflexive transitive closure of binary relations which is not expressible in classical first order logic The Alloy Analyzer Jackson 2012 is a tool that allows one to auto matically analyze Alloy models by searching for counterexamples for a given property using off the shelf SAT solvers There is a visible impedance mis match between the undecidable Alloy language and the decidable language on which SAT solvers operate The gap is bridged by translating Alloy models to propositional models The translation does not come for free it requires users to provide bounds called scopes in the Alloy terminology on the size of data domains The bounded model is the one translated The result of the SAT based analysis is then valid for those semantic structures whose data domains are constrained by the chosen scopes i e if a counterexample is not found one might still exist if larger scopes were chosen While this analysis technique has obvious limitations it is nevertheless very useful when creating a model According to the small scope hypothesis Andoni et al 2002 althou
31. formal parameter of the theory and has type posnat i e positive natural e the minimum and the maximum of the interval determined by the bit width are modeled by the integer constants min fint and max fint defined as exp2 bitwidth 1 and exp2 bitwidth 1 1 respectively e a PVS predicate is defined for delimiting the numbers in this interval 4 Dynamite 56 Dynamite proving system ax Balnai BindingPreservesReachability 1 None product Navigation Navigation d 1 this Domain routing 1 3 uni v this Agent 2 1 Navigation newBinding 1 univ this Identifier 2 1 2 None product Navigation Navigation d 1 this Domain2 dstBinding 1 3 2 univ this Identifier 2 1 Navigation newBinding 1 univ this Identifier 2 2 1 3 None product Navigation univ this Identifier Navigation d 1 this Doma amp Sin2 dstBinding 1 3 1 2 Navigation newBinding 1 univ this Identifier 2 1 4 this AddBinding d 1 d 1 newBinding 1 1 FORALL i this Identifier g this Agent this ReachableInDomain d 1 i g IMPLIES this ReachableInDomain d 1 i g Rule ff U pvs ETA a Dynamite proving system Ax Be kX EEQEXO BindingPreservesReachability 1 no d 1 routing Agent amp newBinding 1 Identifier 2 no d 1 dstBinding Identifier newBinding 1 Identifier 3 no Identifier d 1 dstBinding
32. had to be able of mimic the semantics of every possible Alloy specification and had to have its own complete calculus so that the theorems of that formalism state valid properties on the seman tic Alloy models Once such a formalism was selected we had to design a semantic preserving translation from Alloy to that formalism This chapter is intended to show that the aforementioned approach is correct First we will exhibit the syntax and formal semantics of Alloy The notion of validity of an Alloy assertion will be formally stated as well Then we will focus on the target of the mentioned translation the class of proper point dense omega closure fork algebras PDOCFA The definition of this class will be given along with the presentation of a complete calculus for it Later we will define the translation F from Alloy models to PDOCFA theories Finally we will prove that any theorem in the PDOCFA theory resulting of the translation via F of some Alloy model is valid in it and vice versa interpretability theorem 3 1 Semantics and Syntax of Alloy Signature and field symbols will be called relational variables whilst vari ables bound by quantifiers will be called binding variables We will denote by Names the set of both variable symbols Meanwhile the collection of all relational values sets of tuples of atomic values used to interpret Alloy specifications will be denoted by Rel There are two kinds of atomic values uninterpre
33. in a specification cannot take values off the range determined by bw for each numeric constant symbol c in the Alloy specification we add axioms 2 w 1 lt e and xp ess Given an Alloy integer expression e the Alloy expression Int e denotes the integer atom holding the integer value of e Conversely the Alloy func tion int returns the sum of the integer values corresponding to the integer atoms included in a given Alloy expression For example Int 2 denotes the numeric atom corresponding to the integer 2 which in turn is the result of int Int 2 In PDOCFA we make no distinction between integer values and integer atoms We will use points contained in idenz to represent both kinds on entities We model function Int in PDOCFA with an unary function Int which is defined as the identity We also introduce the function int also unary which models int Axioms all a Z int a a all a ideny idenz int a 0 int 0 0 state that int behaves as the identity on integer atoms and returns 0 for non integer atoms or the empty relation For more complex relational ex pressions int must add the values of the integer points contained in the expression This is captured by the following axiom all r Some r 2 int r int e r w int r e r To support the functionality provided by the Alloy construction sum that allows the user to express a summation of Alloy numeric expressions with free variables rangi
34. in the proof of different assertions For the count of the time effort the time spent in proving each re used lemma only is taken into account once in all the table Assertion Total Model Algebra Time Lemmas Lemmas Lemmas days ConnectedIsEquivalence 79 4 75 10 UnidirectionalChains 52 28 24 5 Reachability 121 62 59 23 Returnability 113 66 47 17 Tab 5 1 Distribution of the workload 5 Evaluation 79 5 2 Evaluating characteristic features of Dynamite The features detailed in Sec 4 2 were evaluated mainly using assertions for an Alloy model by Zave 2006 We begin this section with a explanation of that model Then the evaluation of the features are presented in the following order Sec 5 2 2 presents the evaluation of the sequent pruning techniques Sec 5 2 3 detail the results of testing of the witness generation feature Sec 5 2 4 outlines some remarks about the use of the Alloy Analyzer to validate lemmas new hypothesis and sequents at a given point of the proof 5 2 1 A Running Example Binding in Network Domains The model presented in Zave 2006 deals with the formal definition of a mechanism for binding of identifiers in the delivery of messages in computer networks Thus the model is not a specification of an isolated software or hardware artifact but rather the specification of network services whose implementation may involve several software and hardware agents Th
35. infrastructure called client agents or being part of the infrastructure called server agents Agents can use resources from domains to which they must be attached In order to be able to reach clients from domains pairs address domain are assigned to clients Different sorts of objects can be distinguished in the previous description Domains can create persistent connections between agents Such con nections are called hops Besides the domain that created it a hop contains information about the initiator and acceptor agents taking part in the con nection and also source and target addresses A fact forces these addresses These results were previously reported in Frias et al 2007 74 5 Evaluation 75 to correspond to the agents according to the domain map Multi hop connections are enabled by the servers These connections are called links Links contain information about the server enabling the connection and about the connected hops The reflexive transitive closure of the accessibility relation determined by links is kept by an object Con nections which also keeps the relation established by the links Interoperation is considered a feature of networks Features are installed in domains and have a set of servers from that domain that implement them Among the facts related to features we find that each feature has at least one server and that each server implements exactly one feature Interoperation feat
36. possible to return the received messages is called a returnable domain In order to write conditions ensuring return ability of a domain it is necessary to study how the source identifiers can be modified by the handlers that forward the message because the final source 5 Evaluation 83 NoRec Iter UnSAT Proofs length 969 597 573 Average of formulas per sequent 5 89 6 01 6 20 Occurrences of formulas in proofs no theories 5706 3590 3215 Average of formulas in sequents or theories 34 89 35 01 7 02 Occurrences of formulas in proofs with theories 33807 20903 4023 SAT solver calls N A 770 69 times UnSAT core missed formulas N A N A 1 times UnSAT core avoided detour N A N A 2 Tab 5 2 Measures of attributes for the employed techniques N A not applicable identifier is used by the receiver as the destination of the return message An assertion StructureSufficientForReturnability is also modeled in Zave 2006 Zave 2006 used the Alloy Analyzer to analyze the model and concluded that the previously presented assertions hold for Alloy domains containing at most 2 network domains and 4 elements in each set such as identifiers agents etc Using Dynamite we proved that all these assertions hold inde pendently of the maximum amount of elements in each set 5 2 2 Pruning of goals In this section we present some experimental results we have obtained while applying both pruning techniqu
37. pretty printer Client Server connector off the shelf component existent component Function Call connector lt L gt Request Reply connector Dynamite specific component subsystem Fig 4 3 C amp C view of the Dynamite architecture explained in following sections to this engine as PVS strategies and rules Dynamite proof commands processor in the diagram These extensions are conservatively sound with respect to the logic of PVS We also modified the PVS function for pretty printing in order to allow the user to see Alloy formulas in the sequents as long as it can be done At any point during a proof the user can deactivate and activate the pretty printer when the translation back is possible The Dynamite proof commands processor is responsible for the in teraction with the Java processes that using the Alloy Analyzer validate formulas and goals during the proof suggest the elimination of presumably unnecessary formulas from the sequent and postulate expressions that can be used to instantiate existential quantifiers These Java processes are col lectively referred to as Dynamite Translator As Dynamite is an extension of PVS all the regular PVS proof com mands are available to the user Some of them such as case and inst take formulas or expressions as parameters When the pretty printer is activated the user can write Alloy formulas and expressions as parameters for these comma
38. scopes This shows that this technique is not complete since a neces sary formula might be removed this explains the question mark on safely above and a valid sequent may no longer be derivable This is not a prob lem in itself Hiding formulas based on the user s intuition is not complete 4 Dynamite 64 1 iterativeRemove T A Q 2 for each y T do 3 if proves T y A Q then Procedure proves L A Q checks using the Alloy Analyzer whether sequent AHT holds in model Q In Alloy terms this amounts to checking having as facts the formulas in Q the assertion 4 1 Procedure proves returns true whenever the Alloy Analyzer does not produce a counterexample 4 P T gt 5 end 6 end 7 for each A do 8 if proves T A 6 Q then 9 A A 5 10 end 11 end 12 for each w 2 do 13 if proves T A Q w then 14 Q 20 0w 15 end 16 end 17 end Algorithm 1 The iterative pruning algorithm either Since removing formulas does not allow us to prove previously un derivable sequents refining sequents and theories as explained is a sound rule UnSAT Core Approach Some SAT solvers such as MiniSat E n et al 2006 among the ones provided by the Alloy Analyzer allow one to obtain upon completion of the analysis of an inconsistent propositional theory an UnSAT core An UnSAT core is a subset of clauses from the original inconsistent theory that is also inconsistent
39. sig A sig B in A one sig x1 x2 in A 1 fact x1 in B x2 in B assert needsCoverage some x A xin B Fig 4 8 Simple Alloy model where coverage is needed to prove the assertion The Inputs to the Algorithm line 1 Given a sequent some x T a x that has to be proved the algorithm receives as inputs the set I and the formula some x T a x for which the witness must be produced Initialization lines 2 5 Variable DW will store those witness precandidates that are eventually dis carded Variable result stores the output of the algorithm and its content will be discussed in Section 4 2 5 Variable is initialized with 9 any envi ronment in which I holds o is produced by invoking the Alloy Analyzer The Output variable result Variable result returns a coverage for the formula under analysis A coverage is a set of terms 14 t such that the Alloy Analyzer is able to verify the sequent T a t1 a tz The simple Alloy model in Fig 4 8 shows that coverages are many times necessary In Alloy notation signature B denotes a subset of A and objects x1 and x2 belong to A and since B is contained in A also perhaps to B Notice that the fact guarantees that the assertion is indeed valid Yet no single witness exists In some environments x1 will be a witness and in others the witness will be x2 Notice also that e x1 in B x2 in B holds as per the fact and e x1 in B
40. t Replacing using formula 1 this simplifies to Rbc init 1 2 1 1 XiConPurse c cb cb conAuthPurse 1 XiConPurse cb c cb conAuthPurse Rule grind Trying repeated skolemization instantiation and if lifting This completes the proof of Rbc init 1 2 Rbc init 1 3 B Case Study Proof of Mondex Property 1 Concrete c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 cb archive c archive Rule assert Simplifying rewriting and recording with decision procedures This completes the proof of Rbc_init 1 3 This completes the proof of Rbc_init 1 Rbc_init 2 TCC 1 Concrete c 2 BetwInitState cb 3 c conAuthPurse cb conAuthPurse 4 XiConPurse c cb c conAuthPurse 5 c archive cb archive 6 c ether in cb ether 1 cb in ConWorld Rule hide all but 1 Keeping 1 and hiding this simplifies to Rbc_init 2 1 cb in ConWorld Rule use this cbSubsetSig Using lemma this cbSubsetSig this simplifies to Rbc init 2 TCC 1 cb in cb 2 cb in ConWorld Rule grind Trying repeated skolemization instantiation and if lifting This completes the proof of Rbc init 2 Q E D Run time 2 04 secs Real time 41 89 secs
41. that it is possible to make proofs within the presented calculus with the aid of Dynamite We now present some empirical data that will allow readers to have a better understanding of the usability of the tool The proofs were carried out by a student who had just graduated and had no previous experience neither with Alloy nor with PVS The estimated time he spent in order to master the proof process is the following e 5 days to learn Alloy s syntax and semantics e 15 days to learn PVS including the understanding of the proof rules e 40 days to prove all the assertions contained in the Alloy model e 15 days to prove the nontrivial required lemmas about PDOCFAs These lemmas can be considered as infrastructure lemmas that will be reused in future proofs 5 Evaluation 78 FAL Returnability 1 FORALL hDm hop domain fDm feature domain tDm toDomain tar target rem remote aCn atomConnected con connected oHp oneHop aHp anotherHop rBy reachedBy map map FAL Returnability acc acceptor srv servers exp exported imp imported loc local iTr interTrans Spc space agn agent oEd oneEnd 1 all g1 g2 Client h1 h2 h3 Hop aEd anotherEnd ini initiator hi ini gi AND h2 acc g2 AND att attachments src source hi gt h2 in cConnections con AND FORALL gi g2 Client hi h2 h3 Hop h3 ini g2 AND h3 hDm h2 hDm AND Nav
42. the function cal NumExpr gt Z 3 Formal background 24 formula name let let binding formula conjunction quant bindings formula conjunction block not formula no some 1one one expression formula boolean op formula numeric expr not gt lt gt numeric expr formula gt implies formula else formula pred expression formula lt ee not in expression Me conj block boolean op or amp amp and lt gt iff gt implies quant all no some lone one conj block formula bindings disj var declaration expr declaration expr set decl expr arrow decl expr set decl expr mult expression arrow decl expr arrow decl expr mult gt mult arrow decl expr expression mult gt mult arrow decl expr arrow decl expr mult gt mult expression expression mult gt mult expression mult some one lone set pred identifier Grammar diagram 3 2 Alloy grammar for formulas The formulas in Alloy are mainly constructed from equalities and inclu sions in operator and combining formulas using usual boolean operators conjunction disjunction etc and quantifications It is worth noting that the Alloy language ad
43. these gaps can be bridged in order to provide Alloy with a complete calculus Thus the family of languages presented in this section serves as the core of the languages actually used by the translation and it will be augmented in the next sections in order to support more suitably all the Alloy features 3 Formal background 35 sig Dir extends Object contents Name gt lone Object parent lone Dir Fig 3 1 Declaration of signature Dir Codifying Alloy relations in proper PDOCFA Since the way to define basic elements in Alloy is to declare signatures we first turn to their translation Notice that while function x in Definition 3 2 1 has to be injective it need not be surjective Therefore there may exist ele ments in the base set B that do not encode pairs These elements are called urelements Every Alloy unary relation will be paired with a binary partial identity of urelements i e a binary relation formed only by urelements contained in the identity iden For example the translation of the signature Dir in Figure 3 1 will result in a PDOCFA constant iden Notice that translating Alloy unary relations in this way imposes a con straint on the proper PDOCFAs that could be used as interpretations of the Z PDOCFAs resulting from the translation of Alloy specifications We will say that a proper PDOCFA 2 can support a language L Z PDOCFA which is the outcome of the translation of a given Alloy specification S
44. to prove compatibility we must show that signatures and fields de fined in the Alloy model are given appropriate values according to instance p the relational instance defined from a For signature Sig 1 lt j lt I p idengig iden sig Which clearly belongs to Pw Tree A x Tree A For a field F declared as sig S F S1 gt gt Sk the relation p F defined as s9 51 x Sp so S amp amp s1 E S1 amp amp amp amp sp Sk amp amp 80 51 sy a F belongs to Pw Tree A x Tree A provided ax b is defined as a b We denote by Pw X the power set of set X B CASE STUDY PROOF OF MONDEX PROPERTY In this section we provide the complete proof of a property from the Alloy model for Mondex electronic purse by Ramananandro 2008 as an example of use of Dynamite The property is stated as an Alloy assertion called Rbc init Rbc init 1 some b ConWorld Rbc b cl amp amp BetwInitState b Rule rewrite msg off Turning off rewriting commentary No change on rewrite msg off Rbc init 1 some b ConWorld Rbc b cl amp amp BetwInitState b Rule use Rbc prei Using lemma Rbc_prel this simplifies to Rbc init 1 C CCCCConcrete c amp amp BetwInitState cb l amp amp c conAuthPurse cb conAuthPurse amp amp XiConPurse c cb c conAuthPurse amp amp c archive cb archive amp amp c
45. x2 in B gt some x A x in B holds Therefore the coverage x1 x2 allows us to prove the existential formula This reasoning is easily generalized The proofschema in Fig 4 9 shows that a coverage allows us to prove the existentially quantified formula Building a Witness Precandidate line 7 This is one of the main contributions of Section 4 2 5 The precandidate is built by internalizing Alloy s syntax inside an Alloy model We will present Ax T a tn F o t F3 T a tn F somex d o T a t E a t same applications as below xn F3 IL P Coverage T a ti F somez d o D o t3 a tn F somez d a Il P E afti l o t4 W D o t1 a tn F somez d a P E a t a tn some x d a fe ut DT somex d o Fig 4 9 Use of coverage ti tn y for proving an existential formula Pures q P 89 4 Dynamite 69 sig A one sig cA extends A sig B f A assert existentialAssert some x B a x Fig 4 10 A Sample Alloy Model the technique by means of a simple running example Let us consider the Alloy model presented in Fig 4 10 The model is instrumented with ap propriate signatures functions and predicates In Fig 4 11 we present a fragment of the resulting Alloy model The instrumented model introduces new signatures that model syntac tic internalizations of the source model signatures and fields as w
46. 02 Ch 4 2 a t Thus p T t c1 2 AER Ck k3 2 c1 C2 ER y Ck k2 2 a t LEMMA A 0 2 Let L be a PDOCFA language a proper PDOCFA and p a rela tional instance assigning values from to the constant and variable symbols of L The Alloy instance a built according to Def 3 2 6 satisfies for every Alloy term t with a t C a sigi x x a sigi eife 1 a t a a a Ep T 0 e ifk 1 a t a1 42 ak 01 02 Gk p T t de Proof By Def 3 2 6 a satisfies e for every partial identity symbol iden L a s a a a p iden e for each constant symbol c nor representing a comprehension expression nor being general constants such as univ iden none ideny idenz a c a1 ax a1 02 ax plc where k rank AX c p e for every variable symbol v if v is representing an Alloy variable ranging over atoms a v a such that p v a a else calling k the rank codified in v alv a1 a amp a1 a2 xay p v From the definition of a p satisfies e p iden a a a a s A Complete Proofs of Lemmas from Chapter 3 106 e p c ay a2 xan a1 an a c a a y s t a v a if v is representing an Alloy vari e p v able ranging over atoms a1 a2 ax a1 02 ag alu otherwise We now have an Alloy instance a and a rela
47. 10 1 1 72 4000 amp rep repi amp type pdf ARKOUDAS K 2001 Type w DPLs MIT AI Memo 2001 27 ARKOUDAS K KHURSHID S MARINOV D AND RINARD M 2004 Integrating model checking and theorem proving for relational reasoning In Proceedings of the 7th Conference on Relational Methods in Com puter Science RelMiCS 2nd International Workshop on Applications of Kleene Algebra R Berghammer and B Moller Eds Lecture Notes in Computer Science vol 3051 Springer Verlag Malente Germany 204 213 BECKERT B HAHNLE R AND SCHMITT P H eds Verification of Object Oriented Software The KeY Approach Springer Verlag 2007 BERTOT Y AND CAST RAN P 2004 Interactive Theorem Proving and Program Development Coq Art The Calculus of Inductive Construc tions EATCS Texts in Theoretical Computer Science BLANCHETTE J AND NiPKOW T 2010 Nitpick A counterexample genera tor for higher order logic based on a relational model finder Proceedings of the First International Conference on Interactive Theorem Proving ITP 2010 Lecture Notes in Computer Science 6172 131 146 Springer CLARKE E GRUMBERG O AND PELED D 1999 Model Checking MIT Press DE MOURA L AND BJORNER N 2008 Z3 Am Efficient SMT Solver Pro ceedings of Proceedings of Tools and Algorithms for the Construction and Analysis of Systems TACAS 2008 Lecture Notes in Computer Science 4963 337 340 Springer DUNETS A SCHELLHORN G AND REI
48. 7 Sequent with existentially quantified conclusion 4 8 Simple Alloy model where coverage is needed to prove the assertion 4 9 Use of coverage 14 t for proving an existential formula 4 10 A Sample Alloy Model o o e 4 11 Fragment of Alloy model with internalized Alloy syntax 5 1 Simplified model for addresses agents and domains 5 2 Assertions by Zave 2005 5 8 The initial node of the proof of the assertion Returnability a without pretty printing process being applied and b after the application ofthe pretty printing routine leen 5 4 Main signatures in the model by Zave 2006 5 5 Declaration of predicate DomainSupportsPath 5 6 Extension to signatures in Fig 5 4 o o 5 7 Alloy predicate modeling the addition of a new binding newBinding to a domain d The variable d represents the resulting domain that contains newBinding and all the bindings from d if the new binding could be added to d according to the preconditions stated in the predicate cem eei wee od x eR Rm pe bh A do ees 5 8 Predicate stating the reachability of an identifier in a domain 5 9 A nontrivial assertion BindingPreservesReachability 5 10 A sample model leading to a non atomic coverage witness 5 11 An Alloy instance for assertion coverSample 5 12 Simplified proof tree for assertion BindingPreservesReach
49. 992 PVS A Prototype Verification System Proceedings of the 11th International Conference on Automated Deduction Lecture Notes in Artificial Intelligence 607 748 752 Springer PuDLAK P 2007 Semantic Selection of Premisses for Automated Theorem Proving in Proceedings of ESARLT 2007 pp 27 44 BIBLIOGRAPHY 97 RAMANANANDRO T 2008 Mondez an electronic purse specification and refinement checks with the Alloy model finding method Formal Aspects of Computing 20 1 January 2008 pp 21 39 SHANKAR N 2000 Combining Theorem Proving and Model Checking through Symbolic Analysi in Proc of CONCUR 2000 LNCS Springer 2000 SuTCLIFFE G AND Puzis Y 2007 SRASS a semantic relevance axiom selection system http www cs miami edu Nsim tptp ATPSystems SRASS TORLAK E CHANG F AND JACKSON D 2008 Finding Minimal Unsatis fiable Cores of Declarative Specifications Proceedings of Formal Methods 2008 Lecture Notes in Computer Science 5014 326 341 Springer ULBRICH M GEILMANN U EL GHAZI A AND TAGHDIRI M 2012 A Proof Assistant for Alloy Specifications Proceedings of Tools and Algo rithms for the Construction and Analysis of Systems TACAS 2012 Lec ture Notes in Computer Science 7214 422 436 Springer WEBER T 2008 MaLARea a Metasystem for Automated Reasoning in Large Theories in Proceedings of ESARLT 2007 pp 45 58 WEBER T 2008 SAT based Finite Model Generation for Higher Order Logic Ph D
50. Biblioteca Digital FGEN UBA Mejoras a la demostraci n interactiva de propiedades Alloy utilizando SAT Solving Moscato Mariano Miguel 2013 Tesis Doctoral Facultad de Ciencias Exactas y Naturales Universidad de Buenos Aires www digital bl fcen uba ar Contacto digital bl fcen uba ar Este documento forma parte de la colecci n de tesis doctorales y de maestr a de la Biblioteca Central Dr Luis Federico Leloir Su utilizaci n debe ser acompanada por la cita bibliogr fica con reconocimiento de la fuente This document is part of the doctoral theses collection of the Central Library Dr Luis Federico Leloir It should be used accompanied by the corresponding citation acknowledging the source Fuente source Biblioteca Digital de la Facultad de Ciencias Exactas y Naturales Universidad de Buenos Aires DE CIENCIAS EXACTAS Y NATU RALES UNIVERSIDAD DE BUENOS AIRES FACULTAD DE CIENCIAS EXACTAS Y NATURALES DEPARTAMENTO DE COMPUTACI N Mejoras a la demostraci n interactiva de propiedades Alloy utilizando SAT Solving Tesis presentada para optar al t tulo de Doctor de la Universidad de Buenos Aires en el rea de Ciencias de la Computaci n Mariano Miguel Moscato Director Dr Marcelo Fabi n Frias Consejero de estudios Dr Carlos Gustavo L pez Pombo Buenos Aires 2013 MEJORAS A LA DEMOSTRACI N INTERACTIVA DE PROPIEDADES ALLOY UTILIZANDO SAT SOLVING El an lisis formal de especificaciones de software
51. F W 2010 Automated Flaw Detec tion in Algebraic Specifications Journal of Automated Reasoning 2010 EEN N AND SORENSSON N 2006 MiniSat p v1 14 A proof logging version of MiniSat http minisat se MiniSat html EL GHAZI A AND TAGHDIRI M 2011 Relational Reasoning via SMT Solving Proceedings of Formal Methods FM 2011 Lecture Notes in Computer Science 6664 133 148 Springer 94 BIBLIOGRAPHY 95 Frias M F 2002 Fork algebras in algebra logic and computer science Advances in logic vol 2 World Scientific Publishing Co Singapore Frias M F HAEBERER A M AND VELOSO P A S 1997 A Finite Az iomatization for Fork Algebras Logic Journal of the IGPL Vol 5 No 3 311 319 Frias M F L PEZ POMBO C G AND AGUIRRE N 2004 A Complete Equational Calculus for Alloy in Proceedings of Internacional Conference on Formal Engineering Methods ICFEM 04 Seattle USA November 2004 Lecture Notes in Computer Science 3308 Springer Verlag pp 162 175 Frias M F L PEZ POMBO C G AND MOSCATO M M 2007 Alloy Analyzer4 P VS in the analysis and verification of Alloy specifications In Grumberg O Huth M eds Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2007 Volume 4424 of Lecture Notes in Computer Science Braga Portugal Springer Verlag pp 587 601 GENTZEN G 1935 Untersuchungen ber das logische Schlie en Math
52. Fig 4 5 having o as a proof obligation can be seen as having a as a hypothesis Thus any application of the Cut rule can be seen also as the separation in cases of the proof In the first of them o holds and in the other it does not The Dynamite dps case command improves over the regular PVS case command which implements the Cut rule by using the Alloy Analyzer in order to automatically search for models of the formulas Na AN ui s AN s yer SEN yer Sen where I UI CT A UA C A and at least one of T Z I T Z I AZ A and A A holds Notice that if the original sequent is valid there can not be models for those conjunctions with I I T and A A A It is expected that the introduction of a and a may drop formulas from T and A in each new branch Again the selections I I A and A from T and A must be given by the user By default Dynamite assumes that Del T and A A The existence of the models guarantees that formula o indeed splits into meaningful cases If the Alloy Analyzer does not yield a model for any of the formulas this is reported to the user 4 Dynamite 62 alt in i 1 d 1 dstBinding 1 IdentifiersUnused d 1 newBinding 1 Identifier 3 all i Identifier i in mewBinding 1 Identifier gt i in Address gt i in d 1 space 1 amp amp i in AddressPair gt i addr 1 in d 1 space 1 4 d 1 end
53. The UnSAT core extraction algorithm implemented in MiniSat mostly produces small UnSAT cores The Alloy Analyzer con verts the propositional UnSAT core into an Alloy UnSAT core Torlak et al 2008 i e a subset of the Alloy model that is also inconsistent if the source model was inconsistent Notice that the Algorithm 1 actually computes an Alloy UnSAT core Moreover it computes a minimal Alloy UnSAT core This feature allow us to implement an improved approach for the pruning of sequents When the Dynamite proof command dps hide is applied on sequent I A the system builds an Alloy model containing the original Alloy model under analysis and an assertion on the validity of formula 4 1 Notice that analyzing with the Alloy Analyzer the newly built model Q will not return counterexamples otherwise sequent T A would not be valid We then request the Alloy Analyzer for an UnSAT core of Q 4 Dynamite 65 1 a in i mewBinding d dstBinding 2 no Identifier d dstBinding amp newBinding Identifier 3 no d dstBinding Identifier amp newBinding Identifier 4 not a in i newBinding 5 not a in i d dstBinding 1 some ai Identifier ai in i newBinding amp amp a in ai d dstBinding Fig 4 7 Sequent with existentially quantified conclusion An Alloy UnSAT core Torlak et al 2008 of Q is a subset of Q that is also inconsistent notice
54. Ts is not empty Correspondingly S is inconsistent if Ts is empty DEFINITION 3 1 3 Counterexample Given an Alloy specification S an instance i Zs is a counterexample for an assertion a in S if i E o is false The rest of this section is devoted to give the formal details of the def initions just presented We will begin with the function E and the meta predicate E and then we will focus on how the declarations constrain the instances Expressions and Formulas Although in Section 2 1 we already gave an informal description of the main characteristics of the Alloy language we present here in detail its syntax and semantics as presented in Jackson 2012 Diagram 3 1 shows the grammar for Alloy expressions We denote by amp llY the collection of expressions generated by such grammar Just a few relational operators were not already presented in Chapter 2 They are the domain restriction that behaves as a filter on the tuples of a relation keeping only those which have as a first component an element from a given set the range restriction gt similar to the aforementioned operation but taking into account the last component of the tuples instead of the first and the relational override that allows to update a relation using the 3 Formal background 20 expression none univ iden field rel var expression expression 8 lt gt expres
55. a predicate To do so the specification must include a run command declaration The hierarchy of modules is constructed using the keyword open The modules are able to receive parameters Then when using another module the arguments must be given in the import declaration As this is not a key aspect for the present work the interested reader is pointed to Jackson 2012 where all the details on the matter can be found 3 2 A Complete Calculus Useful for Alloy Users In this section we will present a deductive calculus useful for the verification of Alloy assertions The procedure we will follow in order to present the calculus is the following e We will present the class of proper point dense omega closure fork algebras These algebras contain operations akin to Alloy operations We will also present a complete calculus for this class of algebras The deduction relation in this formalism will be denoted by Frorx e We will present an interpretability theorem from Alloy theories to fork algebra theories An interpretability theorem in this context consists 3 Formal background 30 of a mapping F AlloyForm gt ForkForm mapping Alloy formulas to fork formulas and a theorem proving that T Alloy 7 F y y r I Fonk F a Notice that checking the validity of an Alloy assertion in a specification reduces to the problem of proving a property in the deductive calculus of fork algebras Since the fork a
56. ability 99 APPENDIX A COMPLETE PROOFS OF LEMMAS FROM CHAPTER 3 In this appendix we present the proofs of theorems and lemmas used as the basis of the completeness theorem from chapter 3 From the previous definitions the following lemma can be proved by induc tion on the structure of Alloy terms The lemma besides being necessary for the proof of interpretability shows also in what sense the previous constructions can be considered canonical Notice that both Alloy and relational instances can be homomorphically extended to functions assigning appropriate values to complex terms built from the constants of each language Those functions were called E Def 3 1 5 and Y Def 3 2 3 in chapter 3 For the sake of simplifying the notation we will use in this appendix the same notation for instances and their homomorphic extensions LEMMA A 0 1 Let a be an Alloy instance Let p be a PDOCFA instance defined from a according to Def 3 2 5 Then for every Alloy term t such that a t C a sig X x a sigi we have a a a a t ifk 1 a1 dg kp Ay a2 akp Ea t ifk gt 1 px T t Proof The proof follows by induction on the structure of the Alloy term t The proof is trivial for the constants iden univ and none We present detailed proofs for the cases in which t is an individual variable or t t tg The other cases are easier e if t is an individual variable v if v ranges over atoms
57. al quantification In particular we will show the case of a quantification ranging over atoms The higher order cases are very similar to this one Let suppose that p somex ones a Then BPE PDOCFA iff S E Some x F a ins amp amp R x one s amp amp o by Def of Ed iff S p E Some x F rins amp amp one z amp amp a by R from Def 3 1 6 iff S p E Some x xin iden amp amp one x amp amp F a by T and F from Def 3 2 11 and 3 2 12 iff there exists R Rg such that Spoe rrH R Et in iden and S po reHR Ex one and 3 po xroR Exo F 0 by Def of m F some x ones o It is easy to prove that such R is in fact a point included in iden Let us assume R a a for some a a s Notice that algebra does not depend on the value a assigns to variables Thus is also compatible A Complete Proofs of Lemmas from Chapter 3 108 with instance a x a Moreover from the proof of Lemma A 0 3 if we call p an instance defined from a x gt a according to Def 3 2 5 p poiro R Thus there exists R R such that S peo reoHR m in iden and oP SV x gt R y one and Bp x R EF by Def of Fa iff there exists a a s such that Bp F a ins amp amp one z amp amp o with p as in the previous comment PDOCFA iff there exists a a s such that a xm aj H z ins amp amp one t amp amp a by inductive h
58. argue about its correctness as well as discuss in what conditions the algorithm may fail to produce a candidate Afterwards we will describe several experiments we performed 4 Dynamite 66 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 witnessCandidate I end has the form some x a x DW 0 DW will store the discarded witnesses found so far result E Eo a ta Eo is an environment such that Eo KI while result null do else end end if t else end if there exists a witness precandidate t in then is a valid witness precandidate then result result U t y DW DW U t ECE Ei is the environment in which t failed for each t shrunken WitnessesFrom t do shrunken WitnessesFrom t are the witnesses with the same syntactic structure as t but with every constant c replaced by a constant denoting a subset of c if t is a valid witness precandidate then result lt result U t Y end end if result 0 then if in every environment t contains atom a such that a a holds then a o t amp al else if there is a coverage C C DW then result C end o has been relativized end end if o has been relativized then else end a ta null Algorithm 2 Algorithm for witness candidate generation 4 Dynamite 67
59. atin italic lowercase d d d da etc Alloy declaring expressions Symbols Next we present a list of symbols used trough the document Symbol Description Avda e eR eee Wed acess Defined in page vaa Alloy instance e MAU ES e eed lier tan eee 18 Names Set containing all Alloy variable symbols ssssssss 18 Rel Collection containing all the relations denotable in Alloy 18 A Uninterpreted Alloy atoms 0 c cece cece cnet ene e nes 18 Z Numeric Alloy atoms 0 cece cece He 18 intVal Bijection between numeric atoms and integers sss 18 Ts Legal instances of a specification 0 e eee eee eee eee eee 19 Collection of all Alloy instances see 18 ENS Collection of all Alloy expressions eee 19 E Meaning of Alloy expressions sseeee II 21 Transpose of binary relations 0 cece eee eee eee eee 21 R Transitive closure of relational composition on R 21 R Reflexive and transitive closure of relational composition 21 lt Domain restriction 2i scerese sdb pete et RR eher i a REPRE A Ap ee 21 gt Range restriction 2 lsel bec peu hk Gee Reda lbs Died ded 21 Relational override cece cece eee eee eee teen nee 21 H Cardinality of sets and relations eese 21 E Satisfiability of Alloy formulas sese 24 V Fork oper tor iii ege het erede er eR Ed edat 30
60. ce i must then fulfill that given a definition such as sig S Hn T14 FT TL S Jit 3 4 i 1 The subset signatures can not be abstract The multiplicity qualifiers lone one and some affects the cardinality of the image of the signature symbol on i according to the following statements i S 1 if Sis defined as one sig i S lt 1 if Sis defined as lone sig 3 5 i S gt 1 if Sis defined as some sig Similarly to signatures each field symbol must belong to the domain of the legal instances and the relation mapped to it has to match the arity of the declaring expression A declaration such as sig S f d establish the following restrictions on i a d f dom i and i f C II E univ i 3 6 1 Additionally it also imposes a restriction on i f similar to those imposed by the declaring expression of a quantification i Ri S gt one d f if a d and has no multiplicity keyword VE Ri S gt d f otherwise 3 7 Finally the conjunction block placed after the signature declaration states restrictions on the elements denoted by the signature and fields de clared there Given the declaration sig S fi d1 fm dm Hor Qny a legal instance for it must satisfy if t a for everyist 1 lt i lt n 3 8 where t is a function that given an Alloy formula returns another Alloy formula that only differs from the argument in that every symbol f not preceded by an is replaced by S fj when prec
61. communications Thus signature Identifier is extended by signatures Name modeling unrestricted identifiers and AddressPair for compound identifiers Two fields in the latter addr and name are defined to formalize the structure of complex identifiers The possible bindings in each domain are specified by a ternary relation dstBinding Domain X Identifier x Identifier We introduce dstBinding destination binding by extending the signature Domain and constraining its meaning with a signature axiom Paths are also extended in order to include a new field origDst representing the identifier originally given as destination pred DomainSupportsPath d Domain p Path p source in d routing p generator and p absorber in p dest d routing Fig 5 5 Declaration of predicate DomainSupportsPath 5 Evaluation 81 sig Name extends Identifier sig AddressPair extends Identifier addr Address name Name sig Domain2 extends Domain dstBinding Identifier Identifier all i Identifier i in dstBinding ldentifier implies i in Address implies i in space and i in AddressPair implies i addr in space sig Path2 extends Path origDst Identifier Fig 5 6 Extension to signatures in Fig 5 4 pred AddBinding d d Domain2 newBinding Identifier gt Identifier Precondition the new bindings can be applied in the domain all i Identifier i in newBinding Identifier implies i in
62. d Damon 1996 among others 1 Introduction 4 techniques for automatically proving easy properties but more complex ones require creative steps that must be guided by a human user Proving a theorem can be a difficult and tedious activity even more so if incorrect hypotheses are introduced along the way This situation which is more common than it is desirable is both discouraging and time consuming Notice that every proof step that depends on the wrong hypothesis has to be reconsidered when developing a new proof For instance in order to prove in PVS that a collection of formulas A 61 6m follows from a collection of hypotheses F 1 Y one begins with the sequent T F A Applying inference rules from I A one must reach other sequents that can be recognized as valid for example sequents of the form a o The intuition behind the sequent T A is that from the conjunction of the formulas in I the disjunction of the formulas in A must follow The formulas in T A are called the antecedent consequent of the sequent When an inference rule is applied on a sequent S new sequents S1 9n are produced Proving sequent S then reduces to finding proofs for the in termediate sequents S1 Sn Our experience as users of PVS is that when proving a given sequent the number of antecedents and consequents in intermediate sequents tends to grow This often leads to sequents con taining formulas that are u
63. d in Section 4 2 3 sequents can grow up to a point in which they get very difficult to be understood A handy and time saving feature is the use of the Alloy Analyzer that Dynamite does to prune goals Let us assume we are proving a sequent A where IF 1 and A 61 04 from a theory w1 wn In order to reduce the proof search space we will try to identify formulas from I A and Q that can be safely removed Notice that having fewer formulas actually reduces the proof search space Many proof attempts that could depend on the removed formulas rules for instantiation rewriting or applying strategies are now avoided This reduces the number of instantiations of inference rules that the theorem prover has to consider as well as helps the user stay focused on the relevant parts of the sequent Iterative Approach The first approach we tempted was a rudimentary strategy implemented by the Algorithm 1 It allows us to determine a set of formulas candidate to be removed The algorithm attempts to remove each formula y and analyzes using the Alloy Analyzer whether the sequent obtained after formula y has been removed is valid or not If the sequent is valid then y can be safely removed The previous Alloy analysis requires providing a scope for data domains Therefore it might be the case that the analysis of formula 4 1 does not return a counterexample yet the formula indeed has counterexamples in larger
64. d on the field contents by its declaration assuring that the tuples in contents are formed by atoms from signatures Dir Name and Object in that order can be stated on the corre sponding PDOCFA constant in algebraic terms forcing that pi contents be included in p iden univ p iden V p iden univ ph ideng cce Notice that the relations denoted by terms such as the one just depicted belongs to each PDOCFA structure 2 that can support a language containing the translation of the signatures such as iden iden and iden piece since the set of relations Ry of 2 is closed under the operations of the algebra Regarding individual Alloy variables declared in first order quantifica tions our convention is that these are modeled using relational variables ranging over points The Alloy language also allows the user to write higher order quantifications although the Alloy Analyzer rarely is able to check them Similarly to the translation of signatures and fields the higher order Alloy variables are mapped to PDOCFA variables that are not restricted by the constraint of being a point Additionally we use the number in the PDOCFA variables and constants in order to express the codified rank of the relation denoted by the corresponding symbol In the previous example the number 3 in contents indicates that this constant denotes a binary relation codifying a ternary relation Given an Alloy instance we can characteriz
65. e matische Zeitschrift 39 176 210 405 431 1935 English translation in M E Szabo The Collected Papers of Gerhard Gentzen pages 68 131 North Holland 1969 GORDON M J C 1989 Mechanizing Programming Logics in Higher Order Logic Current Trends in Hardware Verification and Automated Theorem Proving Springer Verlag 1989 HOLZMANN G J 2003 The SPIN Model Checker Primer and Reference Manual Addison Wesley JACKSON D 2012 Software Abstractions Logic Language and Analysis Revised version The MIT Press JACKSON D AND DAMON C A 1996 Elements of style Analyzying a software design feature with a counterexample detector In EEE Transac tions on Software Engineering 22 7 July 1996 JACKSON D SHLYAKHTER I AND SRIDHARAN M 2001 A micromodu larity mechanism In Proceedings of the 8th European software engineer ing conference held together with the 9th ACM SIGSOFT international symposium on Foundations of software engineering Association for the Computer Machinery ACM Press Vienna Austria 62 73 JUNKER U 2004 QUICKXPLAIN Preferred Explanations and Relaz ations for Over constrained Problems In Proceedings of the 19th National BIBLIOGRAPHY 96 Conference on Artifical Intelligence AAAI 04 AAAI Press San Jose Cal ifornia USA 167 172 KAUFMANN T MCCONNELL C VAZQUEZ I ANTONIOTTI M CAMP BELL R AND AMOROSO P 2002 ILISP User Manual Available at http sourceforge
66. e model describes how communicating agent identifiers are bound so that the messages reach their correct destination Properties about the possibility of reaching an agent determinism in the delivery of messages existence of cycles in the routing of messages and the possibility of constructing a return path for a message are formally specified in the model In particular the model studies how these properties are affected by the addition of new bindings between identifiers When an agent wants to send a message to another agent a communica tion is established That communication may involve intermediary agents that just forward the message in its way to its destination The original sender of the message and its intended final receiver are called the endpoints of the communication Endpoints are organized into domains Each do main has its own set of endpoints and uses identifiers to recognize them Identifiers are called addresses Additionally a domain keeps track of how agents are identified by particular addresses Paths describe connections from a generator agent to an absorber agent assuming the generator can be recognized by address source and the absorber by address dest A simplified version of these concepts in Alloy takes the form depicted by Fig 5 4 A domain supports a path if the connections described by the path are consistent with the domain The predicate whose declaration is shown in Fig 5 5 characterizes when a domain support
67. e as of the writing of this document list of publications about the application of PVS to different fields and topics may be found in Rushby 2000 Some of the more relevant characteristics of PVS are the specification language and the semiautomatic theorem prover that serves as the main tool for verification of the models The PVS specification language is based on classical typed higher order logic Besides the built in available types such as booleans integers reals etc the user may define new uninterpreted basic types as well as complex types using constructors for functions tuples sets enumerations etc Since the type system defined by the user is not forced to be decidable the typechecking process may return obligations that can be proven using the PVS prover In fact this feature gives much more expressiveness to the models PVS s theorem prover is a framework that allows the user to perform proofs using sequent calculus Since some of the highlights of Dynamite are the automatic help offered in key steps of the proof in the next section we will explain basic concepts about the calculus PVS s support for user defined proof tactics allows us to define specific rules to take advantage of some aspects of the Alloy logic A comprehensive library of PVS theories covering diverse topics provides wide support to the application of PVS in different areas 2 2 2 Sequent Calculus We already introduced the notion of sequent in the i
68. e latest version of Alloy includes a treatment of integers that avoids some of the overflow issues that the user may face when dealing with such a bounded representation of numbers Nevertheless these operations may not be applied on sets of integers not even singletons but on integer numbers themselves Then Alloy provides a built in function called int to cast from sets of integers to integers So the addition between the count of files in directories d1 and d2 may be denoted by the expression int d1 filesCount add int d2 filesCount 2 Modeling and Analysis of Abstractions 12 When applied to a relation R with cardinality greater than a singleton int R denotes the result of the sum of every numeric atom in R In order to force the field filesCount in the example to hold the count of elements contained by every directory we may use the Alloy operator that returns the cardinality of its argument Thus the mentioned constraint may be stated as the following fact fact all d DetailedDir int d filesCount d contents The backward cast i e from integer numbers to integer atom singletons is performed by the built in function Int So the previous fact could be written as shown below fact all d DetailedDir d filesCount Int d contents 2 1 2 The Alloy Analyzer One of the more appealing features of Alloy is the support for validation given by the Alloy Analyzer Conceptually the Alloy Analyzer may
69. e quantifiers can be skolemized away through the application of proof rules FV and d F respectively The other two rules involving quanti fiers J and VF are intended to deal with the so called existential strength quantifiers Both rules require the presentation of a term that can be used to replace the quantified variable We will call it a witness of the validity of the property We say that the application of these rules is also a critical point because the user has to provide the witness in order to complete the proof Notice that these two critical points are applicable to any sequent calcu lus with rules akin to the ones in Fig 2 3 Nevertheless every logic has its own features which can expose more critical points in the proof process In fact we will see aspects specific to the calculus we propose to verify Alloy assertions in Section 4 2 2 3 Towards a Symbiotic Approach Jackson says about the use of heavyweight methods in the analysis of soft ware abstractions Jackson 2012 Completing a proof with the aid of a theorem prover usually demands an effort an order of magnitude greater than the mod eling effort that preceded it so for most applications it s not cost effective For checking safety critical abstractions however the additional assurance obtained from proof may be worthwhile We wanted Dynamite to be more than just a tradeoff between both approaches the heavy one and the light one We were aiming for a t
70. e those proper PDOCFA that are candidates to interpret it The way to formalize the correlation between Alloy constants and variables and their corresponding PDOCFA elements is to show that it is possible to build a relational instance from an Alloy one so that the correlation between symbols holds The construction is done as follows DEFINITION 3 2 5 Given an Alloy specification S and an instance ag for it we define a PDOCFA language L and a relational instance ph for L such that L is the smallest language fulfilling dom p amp C L and e If S is a signature iden cL and pl ident ss se as S e If F is an n ary field recall that n gt 2 is the only possible case then F L and ph FO a1 02 Gn a1 02 a4 as F e If v is an Alloy variable then 3 Formal background 37 if v range over Alloy atoms vU EL and py v as v as v Notice that the resulting relation is indeed a point else calling n the arity of the Alloy relation denoted by v v L and pi v ar 09X k An a1 a2 m An as v The resulting relation pl v will codify the arity of ag v A Similarly given a proper PDOCFA and a relational instance we can define a sort of canonical Alloy instance DEFINITION 3 2 6 Let L Z PDOCFA be an outcome of a translation from an Alloy specification 9 a proper PDOCFA that can support L and Pa a relational instance a
71. echnique to formulas in the theory was too high Therefore the iterative technique was only applied to formulas occur ring in the sequents being verified along a proof we believe this will be the case most times On the other hand the UnSAT core extraction receives the current sequent plus the underlying theory and automatically refines also the theory This explains the big difference between the average num ber of formulas involved in proofs both in sequents and in the supporting theory using the iterative technique and the UnSAT core based technique Notice that this implies that in each proof step the user and some PVS commands had to consider significantly fewer formulas in order to suggest further proof steps Since proofs are shorter and each sequent contains possibly fewer for mulas the total number of formulas occurring in proofs using UnSAT cores reduces from the original proofs in about 8896 recall that hiding was also 5 Evaluation 85 used in the original proofs but not in an automated way and that formulas from the underlying theory were not hidden For the iterative technique the number of formulas reduces in about 40 While using UnSAT cores required only 69 calls to the SAT solver the corresponding proof steps using the iterative algorithm required 770 calls to the SAT solver without making calls for formulas occurring in the underly ing theory Thus the UnSAT core based technique requires under 1096 of the
72. ection Set difference Cardinality Projection of a tuple Domain of a relation Range of a relation Domain restriction Range restriction Relational override Identity Ri 0 Ra R2 U dom R1 dom R U Ro t t Ri ort Ro Rin R t t R and t Ro R Ro t t Ri and t E R R count of tuples in R IL ai Qi 05 i dom R a 3t Ry and I t a ran R b 3t R and Iln t b A lt R t t R and Il t R gt A t t Ri and IL t H3 lt Ri idena a a a A Being R a n ary relation and S a m ary relation Cartesian product a py Dip gt gt dui ai Ri x Ra jd R and bi bm R Additionally if R is a binary relation s t R C A x A we define Transpose Compositional closures R b a a b R R smallest T s t idena CTATTCTARCT BR R R DEFINITION 3 1 5 Meaning of Alloy expressions The function EVEN s T Rel is defined as shown in tables 3 1 and 3 2 Once defined the syntax and semantics of Alloy expressions we can now proceed to formally define the grammar of Alloy formulas and then turn to their meaning The Alloy formula grammar is depicted in Diagram 3 2 3 Formal background 22 e E e i none 0 univ a 4S Ran i s t a S iden a a a E univ i Int x x E univ iA x Z Int n
73. ed As part of the Alloy model the following assertion is presented assert ReformulateNonEmptinessOK 1 all r univ gt univ some r iff some x y univ x gt y in r Let us consider the assertion obtained by e skolemizing the universal quantifier e substituting iff by implies and e making the antecedent of the implication some r a new hypothesis The resulting model then contains one sig D r univ gt univ fact some D r assert ReformulateNonEmptinessOK some x y univ x gt y in D r Notice that there are two quantified variables Therefore we applied Dynamite in order to provide first a witness for the outer quantification Dynamite returned term D r univ in 161 seconds Once the witness for the outer quantifier was found we looked for a witness for the inner quantifier Since term D r univ denotes a set Dynamite produces the following assertion in order to look for the inner witness fact x1 in D r univ assert ReformulateNonEmptinessOK some y univ x1 gt y in D r Dynamite returns term x1 x1 lt D r as the inner witness in 79 seconds Using these witnesses the assertion is easily verified 5 Evaluation 87 Example 3 The following assertion was presented by Ramananandro 2008 to be analyzed with the aid of the Alloy Analyzer as part of an Alloy model of the Mondex electronic purse assert Rbc init all c ConWorld ConlnitState c implies some b ConWorld
74. eded by t just removes it Paragraphs and Modules Every Alloy specification is constructed as a hierarchy of Alloy modules Each of them is intended to encapsulate a conceptual piece of the whole specification A module may contain signature fact function predicate assertion and run declarations a shown in diagram 3 4 3 Formal background 29 specification module module name import declaration paragraph import declaration open module name paragraph signature declaration fact declaration assertion declation function declaration predicate declaration command declaration command declaration check declaration run declaration Grammar diagram 3 4 Grammar of Alloy specifications and modules The signature declarations were extensively discussed in the previous section The predicate and function declarations are the way to include parametrized named schemes of formulas and expressions in order to facil itate the reuse of concepts As mentioned the fact declarations impose constraints that must be fulfilled by every legal instance of the specification On the other hand the assertion declarations state hypotheses about the universe modeled by the specification These hypotheses can be checked using the Alloy Analyzer To do that a check command declaration must be included in the specification The Alloy Analyzer also can be used to check the consistency of
75. ell as of the relational operators in Fig 4 11 we only include the union of unary relations and the intersection of binary relations The first three lines are exactly the same as the original model They are the semantic base Then the abstract signature Term represents the syntactic terms Its children UnaryTerm and BinaryTerm represent terms denoting sets and terms denot ing binary relations respectively Fields unaryValue and binaryValue relate each term with its intended meaning For example we define a signature A_ Syntax representing the syntactic representation of the signature A in the original module So A_ Syntax is a one signature because there is only one symbol for A and A_ Syntax and A are related with each other trough the field unaryValue In the case of operators see for example the signature UnarySum It represents the union between two terms denoting sets The signature axiom takes care of the meaning of the term restricting the field unaryValue to be the union of the meaning of the sub terms and takes care of its complexity stating that it is equal to the sum of the complexity of both sub terms plus one We also include a number of facts that preclude redundant instances For example fact UnarySumOperandOIsNotUniv states that the first operand in a sum cannot be the universal relation after all the result of the union would be the set univ Several other properties of this kind are included Finally using the Allo
76. ely The symbol denotes the transpose of a binary relation This operation also known as inverse flips around the elements in each pair of a binary relation Transitive closure and reflexive transitive closure of binary relations are de noted by and x respectively For example denoting d a singleton in Dir the term d parent denotes the set containing the parent of d the parent of its parent and so on If we return to the figure 2 2 we may see an anomaly of the model do contains two different objects with the same name no In order to avoid such instances we can add multiplicity keywords to the contents definition The following declaration sig Dir extends Object contents Name gt lone Object parent lone Dir states that for every name n in Name there may be at most one tuple in amu d contents with n as its first element avoiding the instance showed in Fig 2 2 If we turn now to the parent field we already constrained it to allow only one parent per directory But it remains to be said that every directory that is not the root must have a parent and that the root must not have it To impose this kind of restrictions we can add formulas to the model and mark them as axioms called facts in Alloy terminology To construct formulas Alloy provides unary cardinality testing predicates such as the ones explained for signatures being e an Alloy expression one e some e lone e and no e for testing of emptiness e
77. ends Path origDst Identifier one sig a in Address one sig d in Domain2 sig NB in Identifier newBinding set Identifier one sig i in Identifier one sig i2 in Identifier one sig i3 in Identifier fact all disj p1 p2 AddressPair pl addr p2 addr pl name p2 name fact some Agent fact some Identifier fact some Domain fact some Path fact f1 some i newBinding fact f2 i newBinding i2 newBinding 2 fact f3 some i2 newBinding fact f4 i newBinding i2 newBinding assert coverSample some x Identifier one x newBinding check coverSample for 6 but 2 Domain Fig 5 10 A sample model leading to a non atomic coverage witness MN new Binding Fig 5 11 An Alloy instance for assertion coverSample 5 Evaluation 89 Fig 5 12 Simplified proof tree for assertion BindingPreservesReachability revealed by the counterexample Counterexamples also give the user a better grasp on the model because they expose tricky corner cases 6 DISCUSSION LIMITATIONS amp CONCLUSIONS The analysis of abstractions is a central issue of the software development Many formal methods had been developed over the years aimed to attack the problem from different flanks and using diverse techniques Lightweight methods provides the user with automatic techniques to analyze abstractions Nevertheless these analysis are usually partial On the other corn
78. er heavyweight methods provide full analysis but at cost of the need of user guidance In this thesis we tried to bridge the gap between both approaches by pre senting a theorem prover for Alloy that complements the analysis provided by the Alloy Analyzer and at same time takes advantage of it to make the tool less heavy weight A Theorem Prover For Alloy Users Lightweight analysis methods such as Alloy are suitable for a large variety of developments but critical software needs the highest possible level of confidence In this thesis we presented a complete calculus that allows one to prove that Alloy assertions follows from a given model We also embedded this calculus in PVS achieving an interactive theorem prover for Alloy Dynamite in which all the interactions are performed using Alloy syntax Although it could seem just a aesthetic feature at first glance it in fact facilitates the usage of the tool by Alloy users There are two approaches previous to ours in respect to theorem proving of Alloy assertions One is the theorem prover Prioni by Arkoudas et al 2004 Prioni translates Alloy specifications to first order formulas char acterizing their first order semantics and then Athena Arkoudas 2001 an interactive theorem prover for first order logic is proposed to be used in order to prove the resulting theorem While the procedure is sound it is not completely amenable to Alloy users Switching from a relational to a no
79. eractive theorem proving The iterative technique presented in Section 4 2 4 shows resemblance with Pudl k 2007 but Pudl k 2007 uses the Darwin model finder tool to convert first order sentences into function free clause sets No notion of UnSAT cores is provided or used The SRASS system Sutcliffe et al 2007 uses the ideas presented in Pudl k 2007 and complements them with a notion of syntactic relevance but does not make use of UnSAT cores Even members of other communities have faced so similar problems that their solutions can be adapted to our particular interest of trying to find the relevant formulas of a sequent using a model builder For example Junker 2004 presents algorithmic procedures to get the most significative constraints from over constrained problems in the context of Constraint Programming These algorithms are general enough to allow one to adapt them in order to find a solution of our hypothesis selection problem The overall experience of proving theorems using Dynamite was very positive It is remarkable that although the crucial parts of the proofs are still relying on the user using the Alloy Analyzer during the proving process proved to be useful in many ways e Early detection of errors during key steps of proofs helped us save time e The counterexamples retrieved by the Alloy Analyzer helped us im proving our understanding of the problem domain e Having leaner sequents helped us focusi
80. ersUnused d Navigation newBinding univ this Identifier AND this AddBinding d d _ newBinding IMPLIES FORALL i this Identifier g this Agent this ReachableInDomain d i g IMPLIES this ReachableInDomain d _ i g Fig 4 1 PVS embedding of the PDOCFA theorem corresponding to the Alloy as sertion BindingPreservesReachability see Fig 5 9 the theorem BindingPreservesReachability both with and without the application of the pretty printing procedure It is worth noting that not any PDOCFA embedded formula nor expres sion can be pretty printed as a valid Alloy element For instance quantifi cations with no constraints on the quantified variables such as the axiom RA _1 previously shown or expressions containing PDOCFA specific opera tors such as V can not be pretty printed Nevertheless we have defined carefully the embedding so that all PDOCFA formula or expression resulting from the translation of an Alloy element may be pretty printed Embedding Alloy integers The characterization of Alloy integers in PDOCFA presented in Section 3 2 2 can be easily embedded in PVS as a new PVS theory Such an embedding would be suboptimal since it would miss all the support provided by PVS for reasoning about integer arithmetic We will instead use a new PVS theory fint for finite ints parameterized by the bit width This theory profusely uses theory int provided by PVS For example e the bit width noted as bitwidth is a
81. ertion assert underApproximation all v univ v in t1 gt alpha v v in tn gt a v Lack of Witness Precandidates lines 29 33 If a new witness precandidate is not found in the selected environment it may be due to essentially four reasons 1 the existentially quantified formula is not true within the prescribed scopes 2 the bound on the complexity of terms considered is smaller than re quired new witness precandidates might be found if the complexity bound were increased 3 formula a is relativized and therefore part of the available complexity is spent on the relativization term and not enough complexity is left to build a new precandidate 4 the included strategies fail to produce a witness In the first case the lack of precandidates may be due to the exhaustion of all the witness precandidates and the algorithm should terminate without returning a precandidate Similarly in the second case the algorithm should be run again but with an increase in the complexity bound The third case will occur when formula a is relativized Therefore we will remove the relativization in order to enable the search for further witness precandidates In the fourth case new strategies should be added to the algorithm Termination and Correctness Termination is guaranteed because in each loop iteration a new witness precandidate must be generated due to the bound on term complexity only finitely many term
82. es explained in Sec 4 2 4 We begin by presenting some statistics about the model being verified We have verified the model in three different ways namely 1 without using any technique for refining the sequents and theories noted as NoRec for no recommen dation in Table 5 2 2 using the iterative algorithm in order to refine sequents noted as Iter for iterative recommendation and 3 using the UnSAT core extraction technique UnSAT Notice that the way NoRec 1 corresponds to verification using Dynamite 1 0 In Table 5 2 we measure for each technique e Length of proofs measured as the number or rule applications e Average number of formulas per sequent e Sum of occurrences of formulas in proof sequents e At each proof step the user and some PVS commands must con sider sentences from the current sequent as well as the sentences from the underlying theory We then measure the average number of such formulas over the different proof steps These results were previously reported in Moscato et al 2010 5 Evaluation 84 e Sum over the proof steps of occurrences of formulas in proof sequents or from the underlying theories e Number of SAT solver calls for the iterative and the UnSAT core based techniques e Number of times the UnSAT core obtained missed a formula necessary for closing a proof branch e Number of times the UnSAT core allowed us to remove formulas that were used in the
83. f rank e1 2 rank e2 1 1 2 Y eies if rank e1 2 rank e2 gt 1 e1 ideng 1 3 iden ez 0 if rank e1 gt 2 rank e2 1 e1 ideng en Gi 73 iden 2 if rank e1 gt 2 A rank e2 gt 1 3 10 3 We use the construction a b to express that b will stand as an abbreviation of a or vice versa The orientation should be clear by the context 3 Formal background 39 where R S S and R amp 8 R Q R S e1 univ e2 if rank e1 1 A rank e2 1 e1 univ iden V ez if rank e1 1 A rank e2 gt 1 ale 477 ez Bea if rank e1 2 rank e2 1 3 11 eem 1 idenV e2 if rank e1 2 rank e2 gt 1 er vr iden V e3 if rank e1 gt 2 rank e2 1 e1 m iden idenVez if rank e1 gt 2 rank e2 gt 1 Following the previous example if ob is an object atom i e a unary Alloy relation of the form 0b for some ob from signature Object the navigation contents ob produces as a result a binary relation contained in Dir x Name Let us analyze what is the result of applying e on the PDOCFA representation of contents and ob We obtain X contents e ob p by Def of e X contents iden ob 7 p by Def of d a some z Name y Object d xx y in contents A some x Name y Object zx y z xy in iden ob A z x y a my because x z iden A y y ob C iden d a some x Name y Object d xx y in
84. fied model for addresses agents and domains 5 Evaluation 77 assert ConnectedlsEquivalence all c Connections all h Hop h in h c connected amp amp all h1 h2 Hop h1 in h2 c connected gt h2 in h1 c connected amp amp all h1 h2 h3 Hop h2 in h1 c connected amp amp h3 in h2 c connected gt h3 in h1 c connected assert UnidirectionalChains all l Link l agent l oneHop acceptor amp amp l agent l anotherHop initiator l agent l oneHop initiator amp amp l agent l anotherHop acceptor assert Reachability all c Connections g1 g2 Client h Hop a Address d Domain gl h initiator amp amp d h domain amp amp a h target amp amp a gt d in g2 knownAt gt some h2 Hop g2 h2 acceptor amp amp h gt h2 in c connected assert Returnability all c Connections gl g2 Client h1 h2 h3 Hop h1 initiator g1 amp amp h2 acceptor g2 amp amp h1 h2 in c connected amp amp h3 initiator g2 amp amp h3 domain h2 domain amp amp h3 target h2 source gt some h4 Hop h4 acceptor g1 amp amp h3 gt h4 in c connected Fig 5 2 Assertions by Zave 2005 PDOCFA theorem In the right side the pretty printed version of the same sequent is depicted Notice that the pretty printed version closely resembles the Alloy definition Furthermore it can even be compiled with the Alloy Analyzer We have shown
85. g C1 C2 Chy 1 dk 1 a t and dy 1 a t2 iff c1 C2 Cr 1 a t a ta iff 61 02 04 1 e t1 t2 iff 01 09 0 1 a t Thus p T t c1 co e 2 01 C2 Ck 1 a t k gt 2 and ka gt 1 p T Eis t t2 by Def t p T t1 e T t5 by Def T p T t1 ep T t sd by p homo p T 1 iden amp iden amp T t2 by Def e p T t1 iden amp iden p T tz by p homo By inductive hypothesis p T t1 a1 dg ay 1 G2 Qk a t1 A 4 and p T t2 b1 bo x bka b1 b2 bka alta A 5 From A 5 and Def amp iden 8 iden p T t2 a1 ag ab Q1 x xag aba x gs b1 ba 2o bka a tz A 6 From A 4 and A 6 c1 C2 Ck ho 2 P T t iff there exists due to the definition of composition of binary relations di dk 1 such that A Complete Proofs of Lemmas from Chapter 3 105 c1 d x di 11 P T t1 or equivalently as aforementioned c1 di MES di 1 a t4 dy a Chy3 Ck k3 2 a ta and di Ci41 for 1 lt i lt ky 2 From the previous conditions C1 Co X C ka 2 T t iff Ady a 61 00 C 1 di 1 a t and di 1 Ck Ck ka 2 a t2 iff C1 2 Ck 4 k5 2 a ti a te iff 61 02 Ck S 2 e t1 t2 iff 01
86. gh possible it is seldom the case that errors introduced in a model can only be exhibited within large models The aforementioned hypothesis even claims that most software errors can be made explicit by resorting to small domain sizes Therefore if we assume that this hypothesis holds we may infer that many errors introduced when building a model can be discovered by performing bounded analysis using small bounds On the other side of the spectrum of tools we may find the so called heavyweight formal methods named this way after the effort that tools and techniques in this group impose on the user Tools based on interactive theorem provers such as PVS Owre et al 1992 Isabelle Nipkow et al 2002 or Coq Bertot et al 2004 are good examples of this kind of methods which require a significant effort from the user User guidance offers more conclusive analysis techniques but requires trained users Also user guided techniques are often time consuming The bright side of using heavyweight methods is that total analysis can be performed with their assistance even on specifications from languages as much expressive as Alloy or even more expressive For instance there are many complete theorem provers for classical first order logic These include The discussion about the validity or not of the small scope hypothesis is beyond the objectives of this work We point the interested reader to Andoni et al 2002 and Jackson an
87. hat is a valid character in identifiers 4 Dynamite 54 In addition axioms enforcing that these constants have the characteristics mentioned before being a partial universal relation or a partial identity must be included Notice that this part of the translation may generate more axioms depending on the characteristics of the signature being translated abstract one sig extension etc Restricting quantifiers to range over atoms as explained in Section 3 2 2 requires adding for each signature a predicate stating that a relation is a point and it is included in the partial universal relation corresponding to that signature For signature Agent the predicate is this Agent R Carrier bool Point R AND Leq R univ_this Agent When translating field definitions besides the declaration of the corre sponding constant it is necessary to add appropriate axioms stating the restrictions that the definition imposes on the field For example the trans lation of field routing from signature Domain leads to the definition of con stant this Domain routing and to the inclusion of the following axiom this Domain routing AXIOM FORALL this this Domain Leq this Domain routing CartesianProduct univ this Domain CartesianProduct Navigation this this Domain space Navigation this this Domain endpoints This axiom establishes that this Domain routing denotes a relation in which for each tuple d ix g address 7 is in t
88. he space of domain d and agent g is an endpoint for d The translation of predicates functions facts and assertions is direct It is sufficient to translate the formula or expression that defines each of these constructs and add the corresponding predicate function theo rem or axiom to the resulting PVS specification For example assertion BindingPreservesReachability shown in Fig 5 9 is translated to the PVS theorem shown in Fig 4 1 Pretty printing of PDOCFA embeddings in PVS On top of this notation pretty printing algorithms are applied to PVS for mulas occurring during the development of proofs Therefore the user only sees Alloy syntax while working within Dynamite This is one of the impor tant features of Dynamite because it makes it unnecessary for Alloy users to learn another formalism in order to prove the given assertions With the aim of illustrate this feature the Fig 4 2 shows the sequent obtained after a few rule applications from the beginning of the proof of Leq is the predicate corresponding to the set inclusion operator in 3 Navigation is the operator corresponding to and CartesianProduct simulates the behaviour of Cartesian product between relations of arbitrary arity 4 Dynamite 55 BindingPreservesReachability THEOREM FORALL d this Domain2 d this Domain2 newBinding Carrier Leq newBinding CartesianProduct univ this Identifier univ this Identifier DE this Identifi
89. his is more restrictive than Dynamite 1 0 in that Dynamite is not limited to propositional formulas Meanwhile Nitpick Blanchette et al 2010 is used as a counterexam ple generator for the higher order logic supported by the Isabelle theorem prover Nitpick like Dynamite is aimed at detecting non theorems when a proof is initiated Unlike Dynamite Nitpick s application seems to be re stricted to this case Similarly rather than focusing on providing theorem proving capabilities to a lightweight formal method Kong et al 2005 use model checking in order to look for counterexamples before and during the theorem proving process Alternative and more ambitious ways of combin ing model checking and theorem proving are presented by Shankar 2000 Model checkers and theorem provers interact using the latter for local deduc tions and propagation of known properties while the former are employed 6 Discussion Limitations amp Conclusions 92 in order to calculate new properties from reachability predicates or their approximations Since Alloy models are static it is not clear how to employ these techniques Reducing the number of sentences in sequents has been acknowledged as an important problem by the Automated Theorem Proving community The tool MaLARea Urban 2007 reduces sets of hypotheses using machine learning techniques Sledgehammer Blanchette et al 2010 uses auto mated theorem provers to select axioms during int
90. his version of the theorem prover Then we evaluated the features detailed in Sec 4 2 working on the proofs of assertions from some toy models a specification of the Mondex electronic purse system Ramananandro 2008 and an Alloy model of binding in network domains Zave 2006 This chapter shows the results we found in these evaluations and some remarks about it In the next section we explain the test of Dynamite 1 0 The evaluation of the helping features is detailed in Sec 5 2 Both Sections include a description of the models by Zave 2005 2006 since the most of the proofs we performed were taken from those works 5 1 Evaluating Dynamite as a plain prover for Alloy Besides the features explained in Sec 4 2 we wanted to know if Dynamite as a regular sequent calculus theorem prover for Alloy assertions was a usable tool and how many of the lemmas of a significant case study could be proved without having to switch to PDOCFA language We choose to work on the model detailed below because it is a formal model interesting by itself not especially made for this evaluation In this way we try to reduce the possibility of take a biased case study 5 1 1 Case Study Addressing for Interoperating Networks Zave 2005 presented a formal model of addressing for interoperating net works These networks connect agents which might be hardware devices or other software systems Agents can be divided between users of the network ing
91. if it contains a partial urelement identity for each signature and these par tial identities mimic the inheritance hierarchy of the Alloy signatures as explained in Section 3 1 Pg 27 To relate more complex Alloy terms with PDOCFA terms we must find an adequate means for modeling relations of arity greater than two as bi nary relations The operator fork allows us to do this in a simple way For each Alloy relation of arity at least binary holding tuples of the form a1 2 an the corresponding PDOCFA binary relation resulting from the translation process will hold tuples of the form a1 a2 a4 Al though the latter relation is always binary we will say its rank is m if it is the result of the translation of an Alloy relation of arity n Notation 2 Being A an Alloy expression and R its corresponding binary relation in a proper PDOCFA we will call rank R the arity of A Let us illustrate this codification with an example In section 2 1 1 we showed the definition depicted in Figure 3 1 Alloy field contents is a ternary relation Then its PDOCFA counterpart contents satisfies that given an alloy instance ag it is possible to find a relational instance pe where S and L are compatible such that p contents a b x c a b c ag contents Since x is not associative an expression of the form axbxc denotes the object ax bxc 3 Formal background 36 Furthermore the domain restriction impose
92. ig Root extends Dir declares a Root signature included in Dir Notice that because of the one keyword Root is a singleton in every instance To model the relationship between a directory and its parent we could use a binary relation parent C Dir x Dir Relations of arity greater than one are defined by declaring so called fields in a signature For example field parent in the signature Dir shown below denotes a binary relation included in the cartesian product Dir x Dir sig Dir parent Dir In fact that declaration states an extra restriction on the tuples of parent for every atom d Dir there must be one and only one tuple in parent with d as its first element Alloy allows us to include the multiplicity key words mentioned before in order to relax this constraint In our example since every directory except for root must have one and only one parent we need that for every d Dir there be at most one tuple in parent beginning with d This restriction can be stated with the lone keyword sig Dir parent lone Dir In addition to lone one and some previously presented the keyword set may be used to state no restriction at all on the tuples of parent Now once the parent relation has been defined we could write an Al loy expression that relates every directory with its grandparent if it has one The operator for relational composition called navigation in Alloy terminology allows us to wri
93. igation 2 hi ini g1 AND Navigation 2 h2 acc g2 h3 tar h2 src AND Leq composition composition hi one h2 IMPLIES Navigation cConnections con some h4 Hop AND Navigation 2 h3 ini g2 h4 acc gi AND AND Navigation 2 h3 hDm Navigation 2 h2 hDm h3 gt h4 in cConnections con AND Navigation 2 h3 tar Navigation 2 h2 src IMPLIES EXISTS h4 Hop b Navigation 2 h4 acc gi AND Leq composition composition h3 one h4 Navigation cConnections con a Fig 5 3 The initial node of the proof of the assertion Returnability a without pretty printing process being applied and b after the application of the pretty printing routine Recall that relations of rank greater than 2 are encoded as binary ones Therefore it may be necessary to prove properties that deal with the repre sentation These are the only proofs that would not be completely natural to an Alloy user The proof of all the assertions in the model comprises 285 lemmas of which only 12 use this kind of properties Moreover the 12 lemmas actually use 8 different properties of the representation because 3 properties are used at least twice Table 5 1 shows some numerical information about the proofs of the specific assertions The rightmost column shows the time in days the user spent in the proof of each assertion and the lemmas used in it Notice that the sum of the total of lemmas amounts to 365 Therefore 365 285 80 lemmas were re used
94. ignature S it could be swapped for S every appear ance of ideny could be replaced by univ or iden depending on the original Alloy expression idenz could be pretty printed as Int the application of the predicates no some lone and none could be expressed as the juxta position of the name and the argument but keeping aside the parenthesis finally all the numeric operations can be rewritten to appear familiar to the Alloy trained eye 4 DYNAMITE 4 1 Implementation remarks Implementing Dynamite required solving two tasks namely 1 Providing a shallow embedding into PVS of the PDOCFA theories re sulting from the translation of Alloy specifications 2 The careful design of the interaction between PVS and the Alloy An alyzer required in order to provide the user with the new commands offered by Dynamite The proposed solutions are reported in Sections 4 1 1 and 4 1 2 respectively 4 1 1 Embedding the Alloy Calculus in PVS Proving Alloy assertions using Dynamite involves generating a PVS spec ification Said specification is obtained as a shallow embedding Gordon 1989 of the PDOCFA theory resulting from the translation presented in Def 3 2 12 PDOCFA theories obtained from Alloy models have in common their logical part operations their meaning and inference rules presented in Defs 3 2 1 and 3 2 9 while they may differ in the extralogical elements constants axioms theorems that are directly related to the actual
95. ill use the Alloy Analyzer to validate the sequent we should address to prove that this conjecture follows from the original set of hypothesis i e one contents o The Alloy Analyzer will find the coun terexample shown in Figure 4 4 b where can be seen that the root directory is not included in any other directory thus invalidating the sequent under analysis Consequently the application of the rule is aborted Notice that the user has to provide the new hypothesis a and the formu las from T and A suspected to be the ones which o follows from It could 4 Dynamite 61 Dra F A T a F a A a W ona Tia F a A rT F a a A Cut using 7a TFa A Fig 4 5 Strategy to transform the sequent a A into T oo F A seem a requirement for an extra effort from the user but this selection of formulas from TI and A is usually performed at the moment of choosing a even it is generally revealed a few steps after the application of the Cut rule when the specific proof of I a A begins 4 2 2 Introduction of cases As the Cut rule in conventional sequent calculus see Fig 2 3 the appli cation of the Dynamite dps case command splits the current branch into two branches using a provided formula a as a parameter In one of the branches a appears as a new formula in the antecedent and it is placed in the consequent in the other branch DarA TFA a TFA dps case a Notice that following the strategy depicted in
96. in that paper is the need for quantifier instantiation For some of the examples used in Ulbrich et al 2012 the witness generation technique we introduce here was able to produce correct instantiations automatically Another difference arises in the way integers are modeled While El Ghazi et al 2011 Ulbrich et al 2012 depart from the Alloy semantics by considering the standard mathematical model of the integers we stick to the Alloy model where a 2 s complement representation of integers is considered c f Section 3 2 2 A Lighter Interactive Theorem Prover We studied a general sequent calcu lus as an example of a heavyweight analysis procedure and in Section 2 2 3 outlined some of the points of a proof where insight and creativity are spe cially required With these points in mind we developed novel techniques in which the Alloy Analyzer may be used to help the user develop proofs Using SAT solving in the context of first order theorem proving is not new The closest works to Dynamite 1 0 are the thesis by Weber 2008 and the article of Dunets et al 2010 They follow the idea of our 2007 article Frias et al 2007 of using a model generator to look for counterexamples of formulas being proved by a theorem prover Previous articles such as Weber 2006 only focus on using the SAT solver to prove propositional tautologies and use the resolution proofs provided by the SAT solver to guide the theorem prover proofs T
97. int Val cal n i V i v i c e E e e E e e E e i 1 amp e E ein E e2 i ez ea E 1 U E ea i CN ED E e1 i E e2 i 1 2 E 1 i E ea i 1 lt 2 E e1 i lt E e2 i e1 gt 2 E e1 i gt E e2 i n eur Gb E e1 i E ea i e1 m1 mo ea E e1 i x E e2 i mi and ma are ignored E ey i e UL gt E 4 i if e is the function e er en fun flor d1 2g d djes E eji E e1 i E en i otherwise let v e e E e i v gt E e1 i letv nle E e i amp v gt lint Val cal n i y s E e ie ve 0 ifiEo seve Oe E e i otherwise let v1 21 Un In e E let vi x1 let vo x2 Un Lnle i an i Eleyi ifiba QU MEET E e2 i otherwise 01 61 Unien a Gilg 65 505 ie Ue in E e i Fo The function cal NumEzpr Z calculates the value of Alloy numeric expressions using 2 s complement arithmetic Its definition is given in the Table 3 2 Notice that the multiplicity keywords in the arrow expression m and ma in e1m1 m26e2 are ignored here but they will be used when such expressions par ticipate in field and quantified variable declarations to be defined later Tab 3 1 Meaning of Alloy expressions 3 Formal background 23 n cal n i 7e HE e i For numeric constant or variable n n intVal x for the only z s t x i n ni n2 if min lt ni n2 lt maxi ez add ez mini n n maxi if n n2 gt maz ma
98. ion of the proof by revealing those formulas that will be needed to prove the property 5 2 3 Automated Witness Generation In this section we will present 4 examples on which we used Dynamite in order to generate witness candidates automatically We extended Dynamite with a new command solve inst that given a sequent whose consequent is a single existentially quantified formula returns a witness candidate Besides bounding the total complexity of the generated candidates it is also possible to bound the number of times each Alloy operator is allowed to occur in generated candidates In all the experiments each Alloy operator with the exception of the sequential composition that was not bounded was allowed to occur 0 or 1 times We used a computer with the following configuration Intel R Core TM i5 quad core CPU running at 2 67GHz 8GB of RAM The operating system was Debian GNU Linux 6 0 running Kernel 2 6 32 5 Evaluation 86 5 amd64 Example 1 When verifying assertion BindingPreservesDeterminism the following assertion had to be proved assert propl some ai Identifier ai in i newBinding amp amp a in ai d dstBinding Dynamite retrieves as witness the term i newBinding gt d dstBinding a which indeed allowed us to complete the proof It took Dynamite 172 sec onds to retrieve the witness Example 2 In Jackson 2012 Appendix A an exercise involving proper ties of binary relations is propos
99. ique and tool which requires user guidance this usability experiment is not an easy task The test must be carefully planed and carried out in order to get unbiased results Concluding remarks In this thesis we pursue two complementary but dis tinguishable objectives In first place to complement the lightweight ap proach of the Alloy Analyzer to the problem of analysis of abstractions We managed to build an interactive theorem prover designed to Alloy users not only aimed at proving Alloy assertions Besides that we tried to enrich and facilitate the proof process making use of a lightweight approach We attacked several error prone points of sequent calculus proofs providing automatic help to the user We tested the viability and usefulness of the prover and the helping techniques on recognized case studies The result of these tests were very promising The helpful features of Dynamite save uncountable amounts of time by the early detection of errors and the proposal of existential witnesses We believe this thesis serves as a demonstration that by combining dif ferent types of techniques new tools may be developed Such tools are more accurate useful and that brings the power of more conclusive analysis to a broader audience BIBLIOGRAPHY ANDONI A DANILIUC D KHURSHID S AND MARINOV D 2002 Evaluating the Small Scope Hypothesis unpublished Download able from http citeseerx ist psu edu viewdoc download doi
100. iques 1 Recalling that Alloy signatures are constants that may appear in term t term t may fail to be a witness candidate because it includes a signature that is larger than necessary For instance in Zave 2006 we have as part of the signature hierarchy sig Domain3 extends sig Domain2 extends sig Domain Semantically the sets denoted by the signatures satisfy Domain3 C Domain2 C Domain Therefore given a term t of the form Domain routing that fails to be candidate Dynamite explores whether the terms Domain2 routing or Domain3 routing are indeed candidates The technique is applied in lines 13 17 2 The witness candidate could then be the intersection of t with another term We explore this possibility in lines 18 20 Over approximation can be checked with the aid of the Alloy Analyzer by checking the assertion assert overApproximation some v t a v 4 Dynamite 72 Witness Precandidate Failure by Under Approximation lines 22 23 As explained in Section 4 2 5 term t may fail to be a witness precandidate because in some environment e it denotes a set that contains an object that does not satisfy o Yet there might be an already discarded witness t that satisfies a in environment e We then explore if there is a subset of the discarded witnesses that jointly with t form a coverage If a coverage exists it is returned in variable result A coverage is determined with the aid of the Alloy Analyzer by checking ass
101. is to present a complete deductive mechanism for Alloy In order to fulfill this task we will prove an inter pretation theorem of Alloy specifications as PDOCFA theories An inter pretation theorem of Alloy in PDOCFA as described in the introduction to Section 3 2 allows us to map semantic entailment in Alloy to deductions in PDOCFA Said result allows us to use the calculus for PDOCFA in the following way If we want to prove a given assertion in an Alloy model specification M we construct a Z PDOCFA L compatible with M using L we translate a and the facts in M to PDOCFA formulas a and axioms M and prove that a follows from M according to the PDOCFA calculus The initial part of the translation process was already discussed based on the user Alloy specification S we construct a compatible language L by relating fresh constant function and predicate symbols to every signature field function and predicate defined in S Then we collect all the facts in S and translate them into PDOCFA axioms Furthermore all the implicit re strictions imposed for example by the declarations of signatures and fields are also stated in PDOCFA terms and incorporated to the resulting theory as new axioms Additionally the PDOCFA theory must possess all the ax ioms mentioned when we presented the calculus and in the Alloy integers representability section The assertions declared in the original specification S are included also as conjectures
102. ite often For instance predicates are typically used to wrap several related concepts which apply in different sub goals Using one of those concepts requires us to expand the predicate Doing this will not only result in the appearance of the desired formula as hypothesis but the rest of the sub formulas will also appear as part of the sequent To solve this it is common for interactive theorem provers to provide commands for hiding formulas from a goal under the assumption that they will not be used On the other hand the use of this command also presents a risk If by mistake a relevant formula is hidden the user will not be able to close the branch Given a sequent I F A with T 91 7 and A 61 05 result of hiding some formulas the Dynamite command 4 Dynamite 63 dps validate goal automatically searches for counterexamples of the logical implication between the conjunction of the formulas in the antecedent and the disjunction of the formulas in the consequent A vil gt V 05 4 1 1 lt i lt k 1 lt j lt n In this way if a counterexample is found it means that the proof ob jective cannot be reached because the hypotheses are not sufficient to prove the desired property If that goal is the result of hiding some formulas from a sequent for which a similar analysis did not return a counterexample it means that some of the newly hidden formulas were necessary 4 2 4 Pruning of goals As we explaine
103. itical points because they materialize the most error prone moments of the proof Such rules are the Cut rule where an appropriate formula o has to be determined 2 Modeling and Analysis of Abstractions 16 and the rules for quantifiers There are theoretical results that would allow us to leave aside the cut rule The Cut elimination theorem Gentzen 1935 states that proofs can be replaced by usually more complex proofs that do not use this rule But it is of great practical significance in the task of performing a proof using sequent calculus For example when attempting to prove a sequent T F A many times a new hypothesis a is introduced as a means to simplify and modularize the proof In the left new node after the application of the rule T a F A hypothesis a can be used in the proof of the sequent But on the other hand starting from the right new node T F a A it will have to be proved that o follows from some formulas in I and possibly the negation of some other formulas in A This is thus a critical point of the proof because of the loss of time the user could suffer if after finishing the proof of the left subtree with the aid of formula o it turns out that the new hypothesis cannot be discharged from I and A making the previous proof effort useless In case we are confronted with a sequent with either an universally quan tified formula in the consequent or an existentially quantified formula in the antecedent th
104. lation on B is transposition of binary relations is reflexive transitive closure of binary relations Actually these algebras have a complement operation but the latter allows us to define difference with the aid of intersection 3 Formal background 31 V is the fork operation It is defined as SVT a bxc a b S a c ET 3 9 Symbol x in 3 9 stands for an injective function of type B x B B Therefore we assume set B to be closed under x Notation 1 We will often name proper PDOCFA structures using capital gothic letters such as 2 and the set of its binary relations using a bold capital R with the proper PDOCFA it belongs as a subscript for example Ra Syntax and Semantics of the Language Before going further we formally present the languages we propose as the target of the translation of Alloy specifications As usual when working with logical languages we define a family of languages called Z PDOCFA Their main features are the following e A countable infinite collection of variables e A finite collection of constants e Symbols for the constants and operations from def 3 2 1 none univ iden eV 7 amp 33 V e boolean connectives for negation disjunction conjunction amp amp logical implication and material equivalence lt e Universal and existential quantifiers all and some e Syntax constructions resembling Alloy constructions as let erp
105. lgebraic formalism is not exactly Alloy it is essential to discuss to what extent is the new formalism useful for Alloy users This discussion permeates Sections 3 2 1 3 2 3 In Section 3 2 1 we present the fork formalism In Section 3 2 2 we discuss how Alloy quantification is modeled in a formalism where quantifiers range over relations In Section 3 2 3 we present the interpretability result Notice that a particular theory that has to be interpreted in the algebraic formalism is the Alloy theory for integers c f Section 3 2 2 3 2 1 Proper Point Dense Omega Closure Fork Algebras We begin this section by introducing the class of proper point dense omega closure fork algebras Qualifier proper refers to the fact that these algebras are special in the sense that they are particularly close to the semantics of Alloy In effect these algebras have binary relations on a given set B in their universe and operations for union intersection difference navigation transposition and closure of relations as Alloy has DEFINITION 3 2 1 proper PDOCFA A proper point dense omega closure fork algebra on a set B is a structure R amp 0 univ iden V where R is a set of binary relations on the set B closed under the operations is set complement is set union and amp is set intersection is the empty set and univ is the binary relation B x B is composition between binary relations iden is the identity re
106. lloy formulas to PDOCFA formulas 3 Formal background 51 THEOREM 3 2 13 Let XU q be a set of Alloy formulas Then ke lt LF oc ceX r F p Proof gt If F c c NY F q then there exists a PDOCFA such that H F c c U and Y F y From Thm 3 2 10 there exists a proper PDOCFA 3 isomorphic to Clearly 8 E F c 6 Xy and y Y F p Then there must be a relational environment pz such that A pa yg EO c Xj and py xs FU From Lemma A 0 5 there exists an Alloy instance a such that a X and a Z y Thus X 4 y lt If Y j y then there exists an Alloy instance a such that a X and a Y py From Lemma A 0 6 there exists a proper PDOCFA compatible with a From Lemma A 0 4 ps Ex ECO c Xj and py Ex FD Then F c 0 3 F F y m PDOCFA for Alloy eyes Taking into account all the notation remarks introduced along the chapter the reader may note how similar the PDOCFA formulas resulting from the translation process are to the original Alloy formulas A few minimum changes could make those formulas practically indistinguishable from each other These changes could be encapsulated in a process of pretty printing to be applied on the resulting PDOCFA formulas In fact this technique was used in Dynamite the tool in which we implement all the ideas presented in this chapter The pretty printing process could do the following if idens is a PDOCFA constant from an Alloy s
107. mits higher order quantifications although the Alloy Analyzer does not perform analysis on specifications containing such kind of formulas The Alloy language also provides useful syntax constructs such as if then else formulas let formulas user defined predicates and conjunction block formulas In order to improve the readability of the definition of the meaning of Alloy formulas we split it according to the complexity of the formula being analyzed 3 Formal background 25 DEFINITION 3 1 6 Satisfiability of Alloy formulas We say that an Alloy formula a in the context of a specification S is satisfiable w r t an instance i noted as i T ce e e e ps a according to the following statements T un o 3 D o ni lt na Inot lt na TUO not na ni gt na Inot gt na D gt 002 not gt na iE la not a a 8 aor 68 E a amp amp B E a and 8 a lt gt PB iE a iff 8 MESE a implies 8 EM EE e oe let v e a let v qa a E let v x let v n a y iHv i HE a gt else iff iff uf iff uf uf uf uf uf uf uf uf uf uf uf uf uf off la GE O O W ll I IA e gt o A c 2 Kia o a Beba c TAIN YK Il o JUN Ld o an we YH WH WH n2 n2 n2 n2 na i N e eseo zx not i
108. mp amp gt amp formula formula formula else formula let variable symbol expression formula formula all variable symbol formula some variable symbol formula Grammar diagram 3 5 Basic PDOCFA grammar The collection of all possible relational instances for a language L on a proper PDOCFA 2 will be denoted by Jz s For the sake of clarity the super and subscripts in py and Zr s will be used only when necessary We will refer to DI as the collection of all expressions that can be generated by a Z PDOCFA L We will define a meta function that given an expression e INS for a Z PDOCFA L and a relational instance ps calculates the relation denoted by e in the context of the instance ps This meta function can be seen as the homomorphic extension of the relational instance py DEFINITION 3 2 3 Meaning of Z PDOCFA expressions Let L be a lan guage from Z PDOCFA 2 a proper PDOCFA and Ry the set of binary relations from 2 The meta function A a gt Jr gt Ra whose detailed definition is shown in table 3 3 assigns meaning to APDOCFA expressions based on a particular instance Symbolically if e oe and p WSL 2 then AX e p is the binary relation denoted by e in the context of p The notion of semantic truth is defined similarly to the Alloy case 3 Formal background 33 e Xx Px none 0 univ univ iden iden eo palo v pa u
109. n relational language poses an overhead on the user that we are trying to reduce as much as possible The other theorem prover is the one presented by Frias et al 2004 This theorem prover translates Alloy specifications to a close relational language based on binary relations the calculus for omega closure fork algebras Frias 2002 Since the resulting framework is an equational calculus quantifiers are removed from Alloy formulas in the translation process This leads to complicated equations unnatural for standard Alloy users More recent papers El Ghazi et al 2011 Ulbrich et al 2012 also address the problem of verifying Alloy assertions El Ghazi et al 2011 pro pose the translation of an Alloy model to an SMT problem which is solved 90 6 Discussion Limitations amp Conclusions 91 using the SMT solver Z3 de Moura et al 2008 This is a very interesting approach that has some limitations Complex declarative assertions as the ones we deal with in this thesis are unlikely to be solved automatically Also the experimental results show that spurious counterexamples can be produced An approach close to ours is followed by Ulbrich et al 2012 They present the Kelloy prover which is built on top of the KeY first order the orem prover by Beckert et al 2007 Kelloy s embedding into KeY seems to provide greater automation but no integration with the Alloy Analyzer In particular a limitation mentioned
110. ndex Property 110 1 INTRODUCTION Abstractions are foundational parts of the software development process As in many human activities they are the first step of every significant software project Experience has shown that misconceptions in the abstractions re veal themselves as major bugs in the implementation and many times they are very hard to discover until it is too late That is until it is too expen sive or even impossible to repair them Thus such misconceptions must be detected and corrected as soon as possible From simple and informal arrows and boxes diagrams to elaborated for mal methods the variety of conceptual tools used to document communi cate and analyze abstractions is vast and dynamic Dynamic in the sense of their evolution whose trail may be seen in the many techniques and artifacts that have appeared and have been left aside over the years Focusing on the analysis of abstractions we may obtain better results as we move from informal to formal methods Natural language and diagram matic sketches with no formal semantics usually fit adequately to commu nicate basic ideas but they are not a rich field to search for flaws If we just concentrate on the degree of automation offered by the formal methods aimed at the analysis of abstractions the spectrum ranges from fully automatic to fully user driven mechanisms As examples of methods that lie on the former side of the spectrum we can mention M
111. nds The Dynamite proof commands processor is also responsi ble for the translation of those parameters to the corresponding PDOCFA formulas and expressions via the Dynamite Translator Dynamite includes Emacs extensions that allow the user to open an Al loy specification generate the corresponding PDOCFA theories and start 5 Besides inaccuracy the name is maintained for historical reasons 4 Dynamite 59 or redo the proof of any of its assertions among other system level func tionalities All these functions can be accessed through the user menu Additionally Dynamite has an Emacs major mode Alloy mode that provides syntax highlighting for the manipulation of Alloy code 4 2 Features of Dynamite Proving properties can be seen as a handcraft discipline It usually requires a high level of training on the methods adopted to develop the proofs a deep understanding of the concepts formalized in the theory and most of the time lots of patience Even more so if we consider that the person in charge of proving the correctness of the assertions is many times not the person who wrote the model Automatic verification of proofs is somewhat comparable to the spell checker in text editors It does not help you compose a text it just guar antees the absence of syntactic mistakes To be considered useful an inter active theorem prover must be capable of helping the user with the proving process We already men
112. net projects ilisp Kone W OGATA K SEINO T AND FUTATSUGI K 2005 A Lightweight Integration of Theorem Proving and Model Checking for Sys tem Verification in Proc of APSECO5 IEEE MADDUX R D 1991 Pair Dense Relation Algebras Transactions of the AMS Vol 328 N 1 Moscato M LOPEZ POMBO C G AND FRIAS M F 2010 Dynamite 2 0 New Features Based on UnSAT Core Extraction to Improve Verifi cation of Software Requirements International Conference on Theoretical Aspects of Computing ICTAC 2010 Lecture Notes in Computer Science 6255 Springer Verlag Berlin Germany 275 289 Moscato M L PEZ POMBO C G AND FRIAS M F 2014 Dyna mite A Tool for the Verification of Alloy Models Based on PVS ACM Transactions On Software Engineering and Methodology TOSEM To appear NIPKOW T PAULSON L C AND WENZEL M 2002 Isabelle HOL A proof assistant for higher order logic Lecture Notes in Computer Science vol 2283 Springer Verlag Berlin Germany RusHBY J M 2000 PVS Bibliography Available at http pvs csl sri com papers pvs bib pvs bib dvi OWRE S 2008 A brief overview of the PVS user interface 8th Inter national Workshop User Interfaces for Theorem Provers UITP08 Mon treal Canada OWRE S SHANKAR N RUSHBY J M AND STRINGER CALVERT D W J 2001 PVS prover guide Version 2 4 ed Computer Science Laboratory SRI International OWRE S RusHBY J M AND SHANKAR N 1
113. ng on the right proof strategies e Using the Alloy language during proofs contributed to smoothing the learning curve e Automatically finding witnesses for existentially quantified assertions allowed us to shift the focus to higher level proof strategies Limitations and Threats to Validity The work reported in this thesis re vealed also some limitations of Dynamite in its present state In the first place the automation in the proving process is scarce Only few proof steps are automatically solved for instance those referring to typing of relations or to witness candidate generation 6 Discussion Limitations amp Conclusions 93 Another limitation this work revealed was the need for an easily portable knowledge base that as a library of predefined lemmas allows the use of known general properties in the user specific proofs Also it would be very useful to have a mechanism that proposes which of those lemmas are the most likely to be useful at the current point of the proof These are areas in which we are currently working Despite the case study we worked on which spotlights were remarked in Chapter 4 it would be necessary to test the usability of Dynamite with a intensive experiment in the field We believe as stated in various passages of this thesis that the characteristic features of Dynamite simplify the proof developing process but we only tested this assertion with ourselves as the subjects As with every techn
114. ng over sets we will include specific functions and axioms for every such construction present in the user specification If the expression sum v Ej Up En v where v is a numeric expression with n free variables v to vn appears in the Alloy specification we will include in the final PDOCFA specification n function symbols sum sum sum and the n axioms all Xy Xn X3 0 sum X1 Xn 0 amp amp Some X1 gt sum Xi X4 sum Xa Ne Xi Xn ow sum2 e S1 Xo Sn all xy Xs Xn 0 gt sum x1 Xn 20 amp amp Some X gt sum x1 Xn sum x1 Xn e Xn bw qoo unt 809 T 3 Formal background 44 where Tl unt re Xn yy is the result of applying the usual term trans lation T to be detailed below on rv but replacing each Alloy variable v by the corresponding PDOCFA expression e as stated by every v gt ej The theories that model Alloy integers in PDOCFA when bw 1 2 are obtained by adequately instantiating the above theory while at the same time removing axioms 3 13 and 3 14 For instance for bw 1 the axiomatization of the end points becomes Min succ 0 and Max 0 Notice that in this case succ 0 is indeed 1 For PDOCFA models in which the set of integer points is finite the theory correctly captures Alloy s semantics Notice that since the theory admits arbitrarily large finite models by compactness it mu
115. nnecessary for their proof These formulas make identification of new proof steps more complex PVS provides a command hide for hiding hypotheses and conclusions in sequents yet its incorrect use may lead to hiding necessary antecedents or consequents making the proof infeasible Even more while dealing with propositional connectives is straightfor ward in calculi such as the one provided by PVS quantifiers pose a challenge A particularly complex problem is that of finding witnesses when attempting to prove existentially quantified assertions In order to prove that a formula Jr a x holds the user must present a term t such that a t is always true Returning to Alloy for many modeling situations the kind of analysis offered by the Alloy Analyzer is entirely satisfactory In some cases however this analysis may fall short This is evident when building models for critical systems In those cases knowing that no small errors exist in the model is not enough Therefore in this thesis we propose to extend the SAT solving analysis provided by the Alloy Analyzer with a user guided theorem prover based on PVS However although this seems a significant contribution because it gives the user the possibility of reaching complete confidence in the Alloy model the heavyweight task of using an interactive theorem prover threatens the usability of the tool For that reason we also developed automatic tech niques relying on the Alloy Analyzer
116. nsequence Let o an Alloy formula and X a set of Alloy formulas We will say that a is a semantic consequence of Y denoted by X E a if for each instance a such that a o for all o X it also holds that a a Declarations and implicit facts The declarations in the specification state which symbols belong to the do main of every legal instance and also determine facts that must be fulfilled by the image of those symbols In this section we will explore how each declaration affects the constraints imposed on an instance to be called legal Diagram 3 3 shows the grammar of the signature declarations For every signature definition sig S a legal instance i must meet that S dom i and Arity i S 1 3 1 Alloy allows the definition of two kinds of signatures primitive sig natures and subset signatures The primitive signatures can be arranged forming an inheritance hierarchy by using the keyword extends Every legal instance must obey this hierarchy which is achieved by assuring that for each primitive signature S LJ iT i S 3 2 T s t sig T extends S Additionally if the definition of S bears the modifier abstract for the in stance i to be considered legal the inverse inclusion must hold too U i T 2i S when S is declared abstract 3 3 T s t sig T extends S 3 Formal background 28 The subset signatures can be seen as a way to embrace atoms from one or more other signatures A legal instan
117. nstruction But it may be the case that no counterexample could be made no matter how big the scopes would be set So even though the Alloy Analyzer is so useful to develop a consistent specification without errors that could be exposed by generally small examples it cannot give absolute certainty on the correctness of the specification 2 2 A Step Further Heavyweight Methods In some cases such as the development of safety critical systems the partial assurance provided by lightweight methods is not enough and more sophis ticated and complete methods must be used These methods are called heavyweight because they allow one to achieve full confidence in a model but usually require expertise and specific training from the user these many times discourages their use Semiautomatic theorem provers are good examples of heavyweight for mal methods and they are one of the few available choices when dealing with an undecidable logic such as Alloy One of the more prominent ex ponents of this family of tools is the Prototype Verification System PVS Owre et al 1992 2 Modeling and Analysis of Abstractions 14 2 2 1 The Prototype Verification System The Prototype Verification System PVS provides an automated environ ment aimed at the development and verification of complex models Its features make it suitable for a wide variety of application domains where it has been used A comprehensive but perhaps not fully up to dat
118. ntroduction of this work chapter 1 Recall that a sequent is simply a pair of finite sequences of formulas Usually the formulas in the first list of the pair act as hypoth esis and the formulas in the second one act as thesis These sequences are respectively called antecedent usually denoted by T and consequent 2 In the brief description given in the introduction it may be noted that the proofs in a sequent calculus can be seen as a tree When the user starts a proof the proof tree has only one node This tree will grow as the result of the application of the so called proof rules These rules are traditionally depicted as T F Ay whet Diu I which states that the application of the rule R on a sequent with form I F A results in n new sequents I A4 to I F Ap R 2 Modeling and Analysis of Abstractions 15 Tra B A T5 de T BEA THa A OLI Y WH O GP a V B A T avB FA T a F A THa A TEBA Da BRA Taka roa OO ETT EA TF a A E T a F BA THa A DL8FA ps TF o2 8 A D a28 A D ofz t rFA TH afr a A Where t is a term a OR Vr FA ve TE Vr a A FY is a fresh constant and i f UTE a x t is the formula resulting from substitut T a r a F A TH o z t A ing all free occurrence of CYBER AF TF r o A 3 the variable x in with t x a e da a DarA Tra A D1 0 o P2 A LF A1 o o Az SSC Tetras CREAUEAS OC TFA 1 0 12 1 a Ag I Il A ra C r
119. nts but the directory signature is forced to have exactly two 2 Modeling and Analysis of Abstractions 13 run for 3 but exactly 2 Dir It is worth noting that this simulation assisted modeling technique can only be carried out if the analyzer succeeds in the construction of an instance for the given model and scope Complementarily the fail of the analyzer can be understood as an indication of inconsistency of the model Nevertheless this evidence is not conclusive because it may be the case that an instance could be built if the scope is increased Testing of assertions Besides the instance building feature the Alloy An alyzer may be used to test the conjectures stated as assertions This test is done by searching for counterexamples of the assertion In fact this search is another side of the instance builder feature explained earlier The Al loy Analyzer tries to build an instance for which all the facts hold but the assertion does not Again one may include specifications of these analyses in the model itself The following code determines a search for counterexamples of the assertion NoDirAliases with the same scope of the run mentioned before check NoDirAliases for 3 but exacty 2 Dir As in the run case if a counterexample cannot be generated by the analyzer with the provided scopes it does not mean that no counterexample exists Perhaps an increasing of the scopes is needed in order to fulfil the coun terexample co
120. odel Check ing Clarke et al 1999 using tools such as SPIN Holzmann 2003 and SAT Solving using for instance the Alloy Analyzer Jackson 2012 Such analysis methods require little effort on the part of the user and are there fore usually called lightweight formal methods If we confine ourselves to the analysis technique of determining if a model specification is appropriate by analyzing whether certain given properties hold in the model then both model checking and SAT solving can be used to automatically check it But full automation has its price often paid by limitations on the kind of analysis provided or by its lack of scalability In particular both SAT solving and model checking have limitations on the expressiveness of the languages they can analyze This is particularly clear in the case of SAT solving where the source language is propositional logic Also most model checkers support decidable fragments of logics Despite their limitations automatic methods have qualities that make them valuable Even if the model we are working on is expressed in a more expressive formalism we could translate it to a propositional formula in the case of SAT solving or to an automaton in the case of model checking The probably weaker model thus obtained can be automatically analyzed Notice that the result of the analysis of the weaker model can offer partial 1 Introduction 3 information about the original model As an
121. ool 2 Modeling and Analysis of Abstractions 17 with the strength of a heavyweight method but with simple syntax and semantics in order to fit the necessities of as much as possible software developments We wanted to bring complete accuracy but reducing the cost of applying this technique so that it can be applied in many more situations Additionally we intended to establish a synergistic relationship between tools of both worlds so that the human effort to develop a proof could be supported in the critical steps by automated help In the next chapters we will describe Dynamite in detail First we will present the formal foundations of the tool Then we will follow with the implementation description and the explanation of prover helper features included in Dynamite 3 FORMAL BACKGROUND One of the original and main objectives of this thesis was to provide a mechanism to reach full confidence in the analysis of Alloy specifications In particular by offering a mechanism to ensure that an assertion is valid for all possible scopes One way to reach this objective is to provide Alloy with a complete calculus That calculus would allow one to prove that a given assertion can be deduced from the facts of the specification it comes from concluding that it is valid To reduce the amount of work needed to give Alloy a complete calculus we focus our effort in trying to reuse the calculus of a more powerful for malism Such a formalism
122. original proof because of an unnecessary detour In order to focus on the most relevant data we are ignoring proof steps where we prove Type Check Constraints TCCs which in general can be proved in a direct way Also we only applied the techniques either the iterative or the UnSAT core based on 69 proof steps where it was considered relevant to apply the rules Systematic application of the iterative technique for instance each time a new proof goal was presented by PVS would have required in the order of 25000 calls to the SAT solver As a general heuristic we set the scope for all domains in the calls to the Alloy Analyzer to 3 Notice that proofs carried out using any of the techniques for sequent and or theory refinement are about 4096 shorter than the original proof In the original proof as a means to cope with sequents complexity formulas that were presumed unnecessary were systematically hidden While the average number of formulas per sequent is smaller for the original proof having half the proof steps shows that the automated techniques are better focused on the more complex parts of proofs This is supported by the analysis of the total number of formulas that occur in sequents The UnSAT core based technique uses 5696 of the formulas used in the original proof while the iterative technique uses 6396 of the formulas Since the underlying theory in the case study has 29 formulas the over head in applying the iterative t
123. ormal background 50 a F a noe no T e some e some T e lone e lone T e one e one T e i e T e1 T ez ex not ez T e1 T e3 1 in ez T e1 in T e2 e1 lnot in e T e1 in T e2 ni N2 T n1 10 na n not na T n1 T n2 ni lt na T m1 lt T n2 n not lt n2 T n1 lt T n2 tn lt 1009 T n1 lt T na n not na T ni lt T n2 ni gt n2 T m1 gt T n2 n not gt n2 T n1 gt T n2 ni gt na T m gt T n gt n not gt na T n1 gt T n2 la la o 8 a 8 a amp amp B a amp amp B a lt gt B a B a gt p a gt B letv ela let T v T e F a letv 6B la let T v F 8 F a letv nla let T v T n F a let 21 21 Nm 2m a Filet ni x1 let no x2 Am Xm o a gt f else 6 F a gt F 6 else F 0 ai an F ai amp amp amp amp F an allu dla somev d a nov dla all v F v ind amp amp R v d gt o 2 all v T d F a some v F v ind amp amp R v d amp amp a some v T d F a IF some v d o no vi T d F a F all v v d a amp amp o vW 2 v v lonev dla m lone v T d F a F some v d a amp amp all v d a vNv 2 v v onev dla dt lone v T d F a v is a fresh variable a v v is the result of replacing each free occurrence of v by v in a Tab 3 5 Definition of mapping of A
124. p homomorphism a a1 a a1 a ti a1 dg ay 01 02 ak alta by Ind Hyp da a a1 a t4 a1 03 Gr a t3 by Def a a2 gt x AK a a2 ax a t a t2 by Def a a9 gt x aj 4 02 Aka et ta by a homo a aa xak a a2 aka E a t by Def t k gt 2 and k 1 p L t p T ti 2 by Def t p T t e T t5 by Def T p T t iden amp Q iden T tz 7 by Def e p T t1 iden amp amp iden amp p T t5 by p homo Notice that iden p T t2 axb ax b b b p T te by Def axb ax b b a te by Ind Hyp Then A Complete Proofs of Lemmas from Chapter 3 104 Therefore iden amp iden amp p T t2 7 ay amp Gp 3 Ob ay k ag xa bea t3 A By inductive hypothesis p T t 1 bi ba Kee by e bi ba say bki a t4 i A 3 From A 2 and A 3 amp 1 2 cy i1 p T t iff there exists due to the definition of composition of binary relations an object di x x di 1 such that cy di xdg 3 p T t1 or equivalently because of the relationship between p and a ci d1 dg 1 a t1 di 1 a t2 and di C41 for 1 lt i lt k 2 From the previous conditions C1 C2 1 E p T t iff 3d
125. points 1 d 1 endpoints 1 5 d 1 space 1 d 1 space 1 6 d 1 routing 1 d 1 routing 1 7 d 1 dstBinding 1 d 1 dstBinding 1 newBinding 1 8 g 1 in a 1 d 1 routing 1 1 ald in i 1 d 1 dstBinding 1 newBinding 1 2 ali in i 1 d 1 dstBinding 1 3 ali in d 1 dstBinding 1 Identifier Fig 4 6 Example of a sequent obtained after the application of several proof com mands 4 2 8 Hiding sequent formulas During the development of a proof the amount of formulas in the sequent tends to grow For example new hypotheses are introduced when a case splitting is performed The information expressed in these hypotheses may be useful for closing some branches and useless for some others Thus a se quent may contain formulas that are irrelevant to close branches originating in the sequent For example after a branch splitting some formulas may no longer be needed for some of the sub goals and be necessary to prove others In Fig 4 6 we show an open branch that was obtained during the proof of property BindingPreservesReachability reached after a few applications of proof commands Notice that even when the only relevant formulas of the sequent are 1 and 1 the other 9 formulas in the sequent obfuscate the job of proving the assertion turning the sequent very difficult to understand at first glance This is a situation that occurs qu
126. presentation of the restriction stated by the declaration written in Alloy in the following way d R v d one e one v some e some v lone e lone v set e v does not need further restrictions For n a d n1 a d n2 a d2 all v1 v univ di m ma de ES tier Un e Ue e mi Uleft amp amp ma Vrignt amp amp R viest de amp amp R vright d Being n a d n a e1 n2 a d all v1 Un univ e1 mi ma d let Vieft VUn Ung Uright Uny v1 v mi Uleft amp amp mo Uright amp amp R vright d2 Being n a d n1 a d na a e2 all v1 Un univ di mi ma ez let Vieft U Un Ung Vright Un4 v1 0 M1 Uleft amp amp ma Uright amp amp R vieft de Being n a d n a e1 n2 a e2 all v1 0n univ i M1 gt ma 2 let Ujeft VUn Ung Uright Un 7 v1 v mi Uleft amp amp M2 Uright Now we can define the notion of semantic consequence of Alloy formulas 3 Formal background 27 signature decl primitive sig decl subset sig decl primitive sig decl sig qual sig sig extends sig fields conj block subset sig decl sig qual sig sig in name sig fields conj block sig qual abstract lone one some fields field declaration expr Grammar diagram 3 3 Grammar of signature declarations DEFINITION 3 1 7 Semantic co
127. pyaz r tioj Similarly by Def 3 2 5 p z a x a 2 a 6 x a 2 a 6 x gt a x a a Then p 6 x gt r and p also agree for z and hence p O gt r p a LEMMA A 0 4 Let a be an Alloy instance Let p be defined from a according to Def 3 2 5 Let be a PDOCFA compatible with instance a c f Def 3 2 7 Then being y an Alloy formula interpretable in a abe iff amp p F p PDOCFA A Complete Proofs of Lemmas from Chapter 3 107 Proof The proof proceeds by induction on the structure of the Alloy formula y We will concentrate on formulas built from atomic formulas inclusions and existential quantification The other cases are easier e ti in ta For to be well formed t and t2 must stand for relations of the same arity S P E F fa in t2 uf Bp maT 5 in T t3 by Def 3 2 12 uff Sp Ex E 2 T ti T te by Notation remark 5 iff p T te 2 p T t p T t2 by Def of xot and p homo iff p T t1 C p T ta by set theory There are now two possibilities namely either both t t2 have arity 1 or they both have arity k gt 2 Let us continue the proof for the unary case being the remaining case similar We then have p T t1 p T t2 iff a a a a t3 C a a a alta by Lemma A 0 1 iff alt alta by set theory iff a H ti in t2 by Def of e Lets face now the case in which is an existenti
128. quality and inclusion between expressions and in respectively all the usual boolean connectives for negation amp amp for conjunction for disjunction gt for implication lt gt for logical equivalence and several flavors of quantifications The following facts express the aforementioned constrains fact RootHasNoParent all r Root no r parent fact OneParent all d Dir Root one d parent As expected the RootHasNoParent axiom says that for all root directories r the set unary relation in fact of its parents is empty Alloy allows us to express restrictions on the range of the quantified variables as if it were the declaration of a field So the variable d of the OneParent fact ranges over all directories but the root For all such directories the fact assures that they have exactly one parent each We may also add hypotheses about the model and test their validity These hypotheses are called assertions in Alloy For example the assertion 2 Modeling and Analysis of Abstractions 11 NoDirAliases shown below states that every directory may be contained in at most one other directory assert NoDirAliases all o Dir lone contents o Note that while o contents represents all the objects contained in the direc tory o along with each respective name the expression contents o denotes all the directories which include o along with the name by which it is known in each of them Allo
129. r general and useful Constraining PDOCFA Quantifiers to Points When we write an Alloy formula such as all d d Domain d space d space gt d d quantified variables d and d range over Domain objects There is a single signature in PDOCFA namely the one that holds all the relations There fore given an algebra in PDOCFA quantifiers range over all the relations in the domain of the algebra Hence while the Alloy operations have an almost direct counterpart in PDOCFA quantified formulas do not This is when the notion of point become necessary A point is a rela tion of the form a a 4 We constrain the PDOCFAs used to interpret the outcomes of the translation of Alloy specifications to be point dense Maddux 1991 Point density requires set R to have plenty of these re lations More formally speaking for each nonempty relation contained in the identity relation there must be a point p R satisfying p C I We then associate an Alloy singleton a with the point a a As stated in Def 3 2 5 we will associate Alloy signatures with partial identities in PDOCFA Notation 4 We can characterize points as nonempty binary relations that satisfy the property x univ x C iden If we denote the inclusion relation by in as in Alloy the predicate point defined by point p p none amp amp p univ p in iden characterizes those relations that are points We can then map an Alloy formula of the fo
130. r assertion from Zave s model BindingPreservesReachability one of the properties we proved shown in Fig 5 12 A dps hyp command was applied in each grey node It is worth noting that those nodes are the main reason why a branch splitting occurs in that example This shows that a mistake in the introduc tion of a case can invalidate a major part of the proof A similar situation occurs when a lemma is introduced along a proof as a means to modularize the proof effort Proof rule dps lemma calls the Alloy Analyzer in order to analyze whether the introduced lemma is indeed valid The experience in using Dynamite on the case study presented here showed us that this feature is a dramatic improvement with respect to the standard case introduction If a counterexample is found it is shown to the user so the hypothesis or lemma can be corrected using the information 5 Evaluation 88 module fm06 extra2 open fm06 defs sig Agent abstract sig Identifier sig Name Address extends Identifier sig AddressPair extends Identifier addr Address name Name sig Domain endpoints set Agent space set Address routing space gt endpoints sig Path source dest Address generator absorber Agent sig Domain2 extends Domain dstBinding Identifier gt Identifier all i Identifier i in dstBinding Identifier gt i in Address gt i in space amp amp i in AddressPair gt i addr in space sig Path2 ext
131. ra 09 rQASATSERA quy bae bs gap bie wiere T1 b a T2 F A TF Ay B a Ag A CAT er ANT FO Fig 2 3 Proof rules of sequent calculus Consider for instance the proof rules for conjunction AF and FA depicted in Fig 2 3 Rule AF shows that proving a sequent that contains the con junction o B in the antecedent reduces to proving a sequent with both a and in the antecedent in this case a single new sequent has to be proved Similarly rule FA shows that proving a sequent with o in the consequent reduces to proving two different sequents one with o in the consequent and another one with 8 in the consequent Besides the rules for conjunction Fig 2 3 shows examples of rules for standard boolean connectives quantifiers structural rules intended to re order the formulas in the sequent CF FC XF FX W and the Cut rule which can be seen as the formalization of the introduction of some new hy pothesis or as a case separation PVS provides support for a calculus such as this For details in how the proof rules are represented in PVS the reader is pointed to Owre et al 2001b 2 2 3 Critical Points of Sequent Calculus Proofs A closer look at the proof calculus shows that most of the rules in Fig 2 3 can be applied mechanically as in the case of the rules for disjunctive connectives explained earlier Nevertheless there are some rules in which creativity is required We say that the applications of these rules are cr
132. rementioned contributions Organization The thesis is organized as follows In Chapter 2 we present a brief intro duction to the Alloy modelling language the Alloy Analyzer PVS and the sequent calculus provided by it In Chapter 3 we present the formal syntax and semantics of Alloy the Fork Algebras we used as background logic for proving Alloy assertions and the complete calculus for Alloy that will be made accessible through our tool Dynamite In Chapter 4 we describe the way in which the complete calculus presented in Chapter 3 is embedded in PVS as well as discuss important implementation details Also in Chap ter 4 we describe the features of Dynamite Chapter 5 is devoted to report the results of the use of Dynamite on several case studies Some of the goals we envisioned when we started this work were previously addressed either by colleagues or ourselves In Chapter 6 we present a brief review of such related work and discuss some conclusions and further improvements to the tool 2 MODELING AND ANALYSIS OF ABSTRACTIONS When dealing with abstractions their construction and analysis the minimum effort way to cope with these tasks is offered by lightweight methods Lan guages with simple syntax and semantics diagrammatic representations and fully automatic tool support among other characteristics make them ap pealing to a wide spectrum of the public Nevertheless the power of the analysis provided is in most cases not
133. ressions and if then else expressions The constants and variables in these languages are pairs formed by an alpha numeric word w and a natural number k We write them as w Although to use such pairs as constants and variables may seem unnecessary their usefulness will be clear when the translation will be presented The grammar to construct expressions and formulas is shown in dia gram 3 5 As the reader can see there are several aspects shared by Alloy and the languages in Z PDOCFA We look for this similarity in order to simplify the translation process As with Alloy we will use the notion of relational instance in order to assign meaning to expressions DEFINITION 3 2 2 Relational instance for a Z PDOCFA language Let L be a language from Z PDOCFA and 2 a proper PDOCFA A relational instance for L on 2 denoted by pa is a mapping that associates every constant and variable symbol of L with a binary relation in Ry 3 Formal background 32 expression none univ iden constant symbol x expression expression expression amp V expression let variable symbol expression formula expression formula expression else expression constant symbol word number variable symbol word number word la 2 la 2 a 2 2 2 0 9 number 1 9 0 9 formula expression expression formula formula a
134. revisando este documento Nico y Elena GG y M Manu Gracias Marcelo y Charles por la direcci n por el apoyo acad mico y emocional por la ayuda incondicional y por sobre todo por brindarme su amistad Gracias a todas las ramas hojas y hojitas de mi familia GG M Apel Albert Beba Alfredo Silvia C sar Titi Ricky Rochy Coy Nelson Ale Coco Gri Miguel Norman Norma Azul Marta Juan Gracias por todo el amor la fuerza la paciencia Nada hubiera podido hacer sin ustedes Nada ser a Nada valdr a la pena Gracias por ense arme a querer ser una mejor persona en cada momento Dedicatoria A todos los que les agradec En especial a Norma y a Azul El amor que me di la vida en el sentido amplio y el amor que me permite disfrutarla en el sentido amplio Yo soy el faro ahora Nunca m s les va a faltar la luz que yo pueda darles CONTENTS scIntrod ucti nz ee A AT GG UE do ees 3 Modeling and Analysis of Abstractions les 2 1 An Introduction to Alloy o o 2 1 1 Alloy terms and formulas 2 1 2 The Alloy Analyzer 2 2 A Step Further Heavyweight Methods 2 2 1 The Prototype Verification System 2 2 2 Sequent Calculus llle 2 2 3 Critical Points of Sequent Calculus Proofs 2 3 Towards a Symbiotic Approach Formal background 2222s 3 1 Semantics and Syntax of Alloy
135. rm alla Al o to a PDOCFA formula of the form all a point a amp amp a in idena gt a 3 12 3 Formal background 41 where a is the PDOCFA formula resulting from the translation of the Alloy formula a In order to retain the similarity between Alloy formulas and their counterparts we will introduce the following notation all a point a amp amp a in idena gt a alla A a Notice that the above abbreviation equates up to translation of terms the source Alloy formulas and their translation to PDOCFA As showed at the beginning of this chapter there are several ways of stating a restriction on a quantified variable in Alloy but all of them can be adequately expressed in PDOCFA Further Alloy syntax allows higher order quantifications although the Alloy Analyzer is rarely able to manipulate them Following the idea presented all those kinds of quantifications can be expressed in PDOCFA as we will show in section 3 2 3 Alloy Integers in PDOCFA Recall from Ch 2 that Alloy integers are defined relative to a user provided bound Jackson 2012 called the bit width We will denote by pw the arithmetic sum relative to a bit width bw Numeric atoms may appear in relations like regular atoms do In fact they both have the same status To support Alloy integers in Dynamite we enrich PDOCFA theories with new constants functions predicates and their corresponding axioms We add a new partial identit
136. s a path When a message has to be send to an endpoint the identifier used by the initiator to indicate the destination must be bound to the identifier used by the domain to locate the receiver T his binding is done in three ways The simplest one is when the initiator is responsible for performing the binding The message sent has as destination the actual identifier of the receiver The 5 Evaluation 80 sig Agent abstract sig Identifier sig Address extends Identifier sig Domain endpoints set Agent space set Address routing space gt endpoints sig Path source dest Address generator absorber Agent Fig 5 4 Main signatures in the model by Zave 2006 second scenario occurs when the message sent by the initiator is delivered to an agent that is not the intended receiver This agent called handler looks up the corresponding binding updates the destination address and forwards the message The third one is basically the same as the second one but the original destination identifier is composed of two parts which are used by the handler to locate the next agent in the forwarding chain These communication patterns show the need for some distinction in the identifiers used in the model which are stated in the model by extending the previous signatures as depicted in Fig 5 6 Besides addresses there will be unrestricted identifiers called names and complex identifiers used in the third kind of
137. s can be generated Correctness understood as producing a witness regardless of the analysis scopes cannot be achieved due to the undecidability of classical first order logic Therefore the algorithm may produce witness candidates that are not suitable for finishing the proof The effectiveness of the algorithm is evaluated experimentally below 4 Dynamite 73 Limitations This technique heavily relies on the model finding ability of the Alloy Ana lyzer Consequently it shares the same limitations When the search for a candidate begins limits on the search space must are established by fixing a scope Unlike standard Alloy models where the scope only constrains the explored semantic environments Alloy models used for witness generation internalize Alloy s syntax as well Therefore besides providing scopes for data domains we must also provide scopes for syntactic domains maximum amount of occurrences of each operator symbol in the candidates for exam ple If the limits imposed to the search are too restrictive no admissible candidate will be generated Otherwise if the limits are too lax the search can take too much time or lead to an out of memory exception 5 EVALUATION In order to evaluate Dynamite we proceeded in two stages First we took an Alloy model of addressing in the context of computer networks by Zave 2005 and prove five of its assertions using Dynamite without the helping features We call Dynamite 1 0 t
138. s simple as possible so in order to cope with the translation of such expressions we add to the target language L 1 a fresh constant symbol for each such definition in the source Alloy specification and 2 a new axiom that states the restriction imposed in the definition of the com prehension expression Let us see an example Suppose we have an Alloy comprehension expression such as d Dir d contents none with relation contents from signature Dir In order to translate it we add a fresh constant to the target PDOCFA language let s call it C4 and the following axiom to the resulting theory all d d in C amp de contents none Mapping of Alloy terms to PDOCFA expressions The following definition introduces the mapping for terms DEFINITION 3 2 11 Translation of Alloy terms Let M be an Alloy spec ification and L a PDOCFA language compatible with it The function eMAlloy PDOCFA Tm EM gt ET maps Alloy terms to expressions in the language L The detailed definition is given in table 3 4 As usual we will omit the subscripts wherever possible 3 Formal background 48 e T e BE Int idenz Tm iden Int n Int T n iden ideny x T e Being s a signature iii e M T c SPILL 4 dro Being f a field x Fa E f i Ui Vi e T e er 2 T e1 T e2 1 amp ez T e1 amp T ez 1 2 T e1 amp T ez ei 2 T e e T e2 e1 lt ez T ei amp
139. sando el Alloy Analyzer para detectar errores tempranamente refinar secuentes y proponer t rminos para utilizar como testigos de propiedades cuantificadas existencialmente Palabras clave Demostraci n de teoremas interactiva SAT Solving c lculo para Alloy PVS An lisis de especificaciones de software i IMPROVEMENTS TO INTERACTIVE THEOREM PROVING OF ALLOY PROPERTIES USING SAT SOLVING Formal analysis of software models can be undertaken following two ap proaches the lightweight and the heavyweight The former offers languages with simple syntax and semantics supported by automatic analysis tools Nevertheless the analysis they perform is usually partial The latter pro vides full confidence analysis of models but often requires interaction from highly trained users Alloy is a good example of a lightweight method Automatic analysis of Alloy models is supported by the Alloy Analyzer a tool that translates an Alloy model to a propositional formula that is then analyzed using off the shelf SAT solvers The translation requires user provided bounds on the sizes of data domains The analysis is limited by the bounds and is therefore partial Thus the Alloy Analyzer may not be appropriate for the analysis of critical applications where more conclusive results are necessary In this thesis we develop Dynamite an extension of PVS that embeds a complete calculus for Alloy PVS is a well known heavyweight method It provides a semi
140. sion expression expression formula gt implies expression else expression let let binding expression disj var expression formula conj block 3 Int Int numeric expr expression let binding name expression formula numeric ezpr conj block formula rel sig field sig this identifier identifier field this identifier identifier var identifier identifier a z a z 0 9 numeric expr number numeric expr expression expression sum int expression numeric expr add sub mul div rem numeric expr sum bindings numeric expr var let let binding numeric expr number 0 9 Grammar diagram 3 1 Alloy expression grammar 3 Formal background 21 tuples of another relation Alloy also supports more complex syntactic structures such as macro expansions using the let construct if then else and comprehension expressions Previous to the definition of the function E which gives meaning to Alloy expressions we state the notation we use in this document to represent well known relational operations DEFINITION 3 1 4 Relational operations Being R and Ra relations of arbitrary but the same arity say n t a tuple of n elements and A a relation or arity 1 we define Set union Set inters
141. ssigning meaning to constant and variable symbols in L We construct an Alloy specification S and an Alloy instance ag as follows e For every partial identity symbol iden L there is a signature s in S such that ag s a a a p amp iden e For each constant symbol c L not being a logical constant such as univ iden or none there is a field c in S such that as c a1 ak a1 Q2 Gg E sc e For every variable symbol v dom pL a a a a pL v9 ifk 1 a1 ap 01 02 ax ph v otherwise Notice that since L is the outcome of the translation of an Alloy specification we can use that k above as the codified rank of the respective fields and variables DEFINITION 3 2 7 Let a be an Alloy instance A proper PDOCFA is compatible with the instance a if the relational instance pz as defined in Def 3 2 5 is correctly defined in 3 Formal background 38 In Def 3 2 7 correctly defined means that for each symbol s pz s yields a relation in Lemmas assuring this correspondence are presented and proved in Appendix A This way of codifying higher arity relations also impacts in the trans lation of the constants univ and iden Both of them must be related to a binary relation that only holds urelements We will denote such a relation by ideny Another consequence is that some operations in PDOCFA must be mod ified in order to behave as e
142. st admit infinite models as well We leave the study of such models as further work Unlike Ulbrich et al 2012 which departs from Alloy s semantics and considers the standard infinite model for integers we consider 2 s comple ment arithmetic on integers representable using a finite bit width For Dy namite this is not an optional feature of the language but rather the only possible choice In Section 4 2 we will present the main features of Dynamite One such feature is the use of the Alloy Analyzer to look for counterexam ples of properties being verified To be useful counterexamples provided by the Alloy Analyzer must agree with Alloy s semantics as captured in Dynamite s calculus Otherwise counterexamples generated by the Alloy Analyzer would fail as counterexamples for the property being verified with the aid of Dynamite The Point dense Omega Closure Fork Algebras We now introduce a larger class of algebras as the class of models of a finitely axiomatized theory These algebras called point dense omega closure fork algebras we will denote the class by PDOCFA are closely related as will be shown in Thm 3 2 10 to their proper counterpart In order to present the theory we will present the axioms and the proof rules The axioms and inference rules for the calculus are given in the following definition DEFINITION 3 2 9 PDOCFA calculus The calculus for point dense omega closure fork algebras is characterized
143. suele atacarse desde dos enfoques usualmente llamados liviano y pesado En el lado liviano en contramos lenguajes f ciles de aprender y utilizar junto con herramientas autom ticas de an lisis pero de alcance parcial El lado pesado nos ofrece lograr certeza absoluta pero a costo de requerir usuarios altamente capaci tados Un buen representante de los m todos livianos es lenguaje de modelado Alloy y su analizador autom tico el Alloy Analyzer Su an lisis consiste en transcribir un modelo Alloy a una f rmula proposicional que luego se procesa utilizando SAT solvers est ndar Esta transcripci n requiere que el usuario establezca cotas en los tamanos de los dominios modelados en la especificaci n El an lisis entonces es parcial ya que est limitado por esas cotas Por ello puede pensarse que no es seguro utilizar el Alloy Analyzer para trabajar en el desarrollo de aplicaciones cr ticas donde se necesitan resultados concluyentes En esta tesis presentamos un c lculo basado en algebras de Fork que per mite realizar demostraciones en c lculo de secuentes sobre especificaciones Alloy Tambi n hemos desarrollado una herramienta Dynamite que lo implementa Dynamite es una extensi n del sistema de demostraci n semi atom tico PVS m todo pesado ampliamente utilizado por la comunidad As Dynamite consigue complementar el an lisis parcial que ofrece Alloy adem s de potenciar el esfuerzo realizado durante una demostraci n u
144. suited to critical developments On the other hand heavyweight methods allow the user to perform com plete analysis on the abstractions but at the cost of losing the automation Clever interactions at crucial points of the analysis process are often indis pensable to fulfill the task This makes the application of such methods an error prone activity Furthermore besides requiring more user effort they usually demand a high level of training which in turn reduces the spectrum of public able and willing to use them This chapter is intended to contrast both approaches by showing rep resentatives of each kind First we will present Alloy as an example of a lightweight method We will introduce rudiments about the language and its associated analysis tool the Alloy Analyzer The way in which the ana lyzer can be used as an assistant in the modeling process will be explained Next we will introduce the Prototype Verification System PVS an en vironment supporting the development and the analysis of specifications based in theorem proving for classical higher order logic We will discuss the underlying formal machinery implemented by PVS the sequent calcu lus 2 1 An Introduction to Alloy In this section we describe the Alloy modeling language and the Alloy Ana lyzer with the level of detail required in order to follow this work For a thor ough description we point the reader to the book Software Abstractions Logic Language and
145. te that expression as parent parent As described before a directory can contain files and directories Nat urally by now we hope the files will be represented as a new signature File So using signature inheritance one can group directories and files in an abstract concept Let s call it object abstract sig Object sig File extends Object The keyword abstract states that Object will only hold elements from in heriting signatures 2 Modeling and Analysis of Abstractions 9 aw d am contents do do no do do no fo d1 no do Y ay d contents no do no fo EM 1 Fig 2 2 Example of navigation between non binary relations Recalling that every object must have a name local to the directory con taining it the contents of a directory can be represented as a ternary relation contents C Dir x Name x Object In Alloy relations of arity greater than 2 are also declared as fields but using the arrow operator gt sig Dir extends Object contents Name gt Object parent lone Dir do no fo di no do contents do no do Every tuple d n o contents means that o is contained in d under the name n Along the last showed declaration of Dir a possible instance for it is depicted There dy and d are atoms from Dir no from Name and fo from File Lets assume we have an Alloy expression d denoting a singleton unary relation that holds the atom dy
146. te that unary relation in any expression of the specification Fig 2 1 b shows the value taken by Name in three different and valid instances for the model M Alloy provides multiplicity keywords in order to restrict the relations introduced by a signature These keywords are some the relation can not be empty one there can be only one tuple in the relation lone the relation can have at most one tuple The table 2 1 shows which of the instances of Fig 2 1 b are valid if each multiplicity keyword was added in turn to the declaration in Fig 2 1 a Let us suppose we want to model a simple file system using Alloy The main concepts are directories can contain files and other directories every element inside a directory can be referred to using a name that can vary in Ko u uo e 3 Sd 5 NG SS S ES b ae ae lt E E e EY o P a ay Nam X Y KB lt lt ou ay Name no Y Y Y Y X invalid da Name X X V V Tab 2 1 Signature multiplicity keywords example 2 Modeling and Analysis of Abstractions 8 other directories there is only one root directory every non root directory must have a parent i e the directory containing it The directories could be represented by means of a signature Dir as we did it with the names previously Now we have a distinguished directory the root To embody this feature Alloy allows us to establish inheritance relationships between signatures Then one s
147. ted in the previous section 7 p univy Y in Point and a few more intended to facilitate the translation process All of these elements are defined using the elements mentioned in the preceding items For example the binary operation amp is defined as follows Cross x y Carrier Carrier fork composition Pi x composition Rho y PVS natively provides a standard sequent calculus see Owre et al 2001b for details The only rule that has to be incorporated is the w rule see Def 3 2 9 Using the support for natural numbers offered by PVS this rule is expressed as a PVS axiom Embedding of the Extra logical Aspects of a PDOCFA theory We present the translation of the extralogical part of the specification in two steps We focus first on PDOCFA constants coming from Alloy signatures and fields and their properties We subsequently deal with the translation of functions predicates axioms and assertions When translating an Alloy signature definition it is necessary to intro duce a new symbol for the partial universal relation over atoms from that domain and another new symbol for the partial identity formed with those atoms For instance the translation of signature Agent yields the PVS definitions univ this Agent Carrier the partial universal of Agent atoms iden this Agent Carrier the partial identity of Agent atoms Notice that in PVS everything at the right of the symbol is considered a comment and t
148. ted atoms A and numeric atoms Z They only differ in the existence of a bijection named int Val from the latter to the set of integer numbers An Alloy instance or Alloy environment is a mapping i Names gt Rel that assigns meaning to variable symbols We denote by Z the collection of all instances 18 3 Formal background 19 Given an Alloy expression expr and an Alloy instance i the function E gives meaning to expr based on i Correspondingly given an Alloy formula o and an Alloy instance i we will define a metapredicate that will indicate whether the formula o is true or false with respect to the instance i noted as i H a Both E and E will be formally defined in the next section Notice that an instance does not need to be total but we restrict the domain of the instances with respect to a given specification in the next definition DEFINITION 3 1 1 Legal instances of a specification The collection of legal instances of a given Alloy specification S denoted by Zs contains every instance i such that a every constant symbol defined in S belongs to the domain of i b there exists an n N s t all the integer numbers representable in a 2 s complement representation of n bits are defined in i more formally i j intVal 1 j for each integer j 2971 2 7 1 a is true for every fact o in S e c DEFINITION 3 1 2 Consistence An Alloy specification S is consistent if
149. that inconsistency is defined up to the considered scopes The UnSAT cores retrieved by the Alloy Analyzer do not need to be minimal but many times are proper subsets of the premises and consequents of the sequent and theory under analysis Command dps hide then hides all those formulas in Q T and A that are not part of the retrieved UnSAT core The relevant formulas in the sequent depicted in Fig 4 6 formulas 1 and 1 are automatically identified by applying this command 4 2 5 Automated Witness Generation When proving the property BindingPreservesDeterminism the sequent depicted in Fig 4 7 is produced Notice that the formula in the consequent is exis tentially quantified According to the proof calculus depicted in Fig 2 3 in order to prove the sequent we must find a suitable witness i e a term that when substituted for variable ai makes the resulting sequent provable DlFA z t A IT Ges A A In order to reduce user intervention in this section we will present an effective technique that uses the Alloy Analyzer in order to automatically generate witness candidates Also we will present several examples where the application of the proposed technique yields the required witnesses In Alg 2 we present the algorithm we use for witness candidate genera tion Recall that environments are the semantic structures in which Alloy models are evaluated In the following paragraphs we will explain the algorithm and
150. the Alloy Analyzer in order to 4 Dynamite 60 1 lone contents o parent a b Fig 4 4 Example of use of the rule dps hyp analyze whether sequent I a A follows from the model If a counterex ample is found within the provided scopes it is reported to the user and the hypothesis is removed Example 1 Assume we are trying to prove the assertion NoDirAliases pre sented in Section 2 1 1 Pg 11 This assertion shown below states that all directory may be contained at most in one directory assert NoDirAliases all o Dir lone contents o As the first step of our proof we need to apply the command corresponding to the rule FV see Figure 2 3 in order to get rid of the universal quantifi cation After the application of such command we would face the sequent depicted in Figure 4 4 a Sometimes stronger properties are easier to prove We could try to prove that one contents o holds or that no contents o holds In other words if we could prove that contents o is always empty or it always has only one element we could complete the proof of the assertion In order to test this strategy we can use the Dynamite command dps hyp one contents o Under this configuration the sets of formulas mentioned in the descrip tion of the rule dps hyp are the following T A lone contents o a one contents o As its default behaviour this rule takes I Tr and A So Dynamite w
151. the properties in Fig 5 2 using Dynamite Fig 5 3 illustrate the pretty printer feature In the left side can be seen the initial node of the proof of the assertion Returnability as the plain PVS embedding of the corresponding 2 The complete model can be obtained from http www2 research att com pamela svcrte html 5 Evaluation 76 sig Agent attachments set Domain sig Server extends Agent sig Client extends Agent knownAt Address Domain sig Domain space set Address map space Agent sig Hop 1 domain Domain initiator acceptor Agent source target Address abstract sig End one sig Init Accept extends End sig Link agent Server oneHop anotherHop Hop oneEnd anotherEnd End H oneHop anotherHop oneEnd in Init gt agent oneHop initiator oneEnd in Accept gt agent oneHop acceptor anotherEnd in Init gt agent anotherHop initiator anotherEnd in Accept gt agent anotherHop acceptor one sig Connections atomConnected connected Hop gt Hop abstract sig Feature domain Domain servers set Server sig InteropFeature extends Feature toDomain Domain exported imported remote local set Address interTrans exported some gt some imported H domain toDomain amp amp exported in domain space amp amp remote in exported imported in toDomain space amp amp local in imported remote interTrans local Fig 5 1 Simpli
152. tion in section 2 2 3 a couple of critical points of the proof process where the user might need assistance Those points heavily rely on specific rules nevertheless there are other aspects related to the mechanic of the calculus to the way in which the current sequent is evolving that also obstruct the developing of the proof Dynamite is intended to be more than a proof checker It offers help in situations such as the previously mentioned In order to do so it uses the Alloy Analyzer in different ways that are to be detailed in the following sections This makes Dynamite much more than syntactic sugar on top of PVS 4 2 1 Introduction of Hypotheses and Lemmas As explained in section 2 2 3 the application of the Cut rule can represent the introduction of a new hypothesis In PVS the user can introduce a new hypothesis in such a way using the rule case Still we may want to go a step further and gain some confidence on the suitability of the introduced hypothesis Does it actually follow from some of the formulas already in the sequent It is frustrating to realize after finishing the proof with the aid of the new hypothesis that it cannot be discharged deeming the previous proof effort useless In order to reduce the risk of introducing inappropriate hypotheses Dynamite introduces the rule dps hyp Dar A Fa A desea where I C T A C A and at least one of T 4 I and A Z A holds The use of rule dps hyp triggers a call to
153. tional instance p that satisfy the con ditions in Def 3 2 5 Notice then that is compatible with the Alloy instance a From Lemma A 0 1 for every Alloy term t with a t C a sigi x x a sigi e ifk Ll p T t a a3 a a t y e if k 5 1 p T t a1 a2 ag a1 2 a a t It then follows that for every such term e ifk 1 a t a a a p T t e ifk gt 1 a t a1 ae ax 41 2 xak p T t y The following lemma will be used in the proof of Lemma A 0 4 LEMMA A 0 3 Let a be an Alloy instance Let p be a relational instance defined from a according to Def 3 2 5 Let fa be a PDOCFA compatible with instance a c f Def 3 2 7 Let a be an atom from a signature s a a x a an Alloy instance that can only differ from a in the value of the variable x p a relational instance defined from a and a PDOCFA compatible with a Finally let r a a iden be a point Then Sap D tro Tr Ee 6 df Sab PDOCFA B PDOCFA Proof In order to prove the lemma it suffices to show that Ja Sa and p e x r p According to Defs 3 2 5 and 3 2 7 the construction of algebra Fa does not depend on the value a assigns to variables Therefore it is immediate that Sa T Fa On the other hand for all signatures fields and variables distinct of x it is clear that p O x gt r and p agree For variable x we have peireor
154. ures are then characterized by signatures Feature and InteropFeature in Fig 5 1 where a simplified description of the signatures that formalizes the model detailed here is presented An interoperation feature translates addresses by means of the relation interTrans between different domains This is necessary because whenever a client from the feature s domain wishes to connect to a client attached to a different domain it must have a target address it can use in its own domain space Of course the target client must have an address in each domain from which it is to be reached Different facts are introduced in order to fully understand an interoperation feature behavior and the following assertions are singled out e ConnectedlsEquivalence asserting that field connected is indeed an equiv alence relation reflexive symmetric and transitive e UnidirectionalChains asserting that two hops are connected through a link in an ordered manner one can be identified as initiator and the other one as acceptor e Reachability asserting that whenever a client c publishes an address a in a domain d a d c knownAt clients c from domain d can effectively connect to c e Returnability asserting that if a client c accepted a connection from another client c then a hop from c can be extended to a complete connection to client c The Alloy description of the previous assertions is given in Fig 5 2 5 1 2 Evaluation We proved
155. users Prior to presenting the formal definition of the formula mapping we introduce more notation with the aim of improving its readability Notation 5 We will use predicates for testing cardinality analogous to those pro vided by Alloy no e e none some e 2 el none one e card e succ 0 lone e no e one e The operator of inclusion which was already used is in fact an abbreviation f e1 neta 1 82 Also we will use abbreviations for the negation of equality inclusion and numeric comparison 7 e1 X es 2 1 X 23 ll 1 2 e1 ea Mer en ez gt ez E e lt ez e1 lin ea z ex in ea e1 gt e S e eg e1 e2 e1 ez es lt e2 1 ea Les lt e2 e gt eg Mei gt e ez m es Her gt e2 DEFINITION 3 2 12 Translation of Alloy formulas Let M be an Alloy specification and L a PDOCFA language compatible with it The function Alloy PDOCHA Fm D gt DT maps Alloy formulas to PDOCFA formulas in L The detailed definition of F y r can be seen in table 3 5 For the sake of clarity we will be omitting the subscripts when possible Notice that the result of the translations of Alloy quantifications over atoms although different from those explained in formula 3 12 are equiva lent to them We next will prove the following completeness theorem recall that the turnstile symbol notes the derivability relation in the calculus of PDOCFAs 3 F
156. xpected for Alloy Such operations are those whose result differs in arity from their parameters namely navigation and cartesian product We define in PDOCFA two new operations denoted by e for navigation and XX for cartesian product that preserve the previously given invariant Before doing so we introduce some notation Notation 3 In a proper PDOCFA the relations 7 and p defined by iden Vuniv x and univViden p behave as projections with respect to the encoding of pairs induced by the injective function x Their semantics in a proper PDOCFA 2 whose binary relations range over a set D is Xy 7 py axb a a b B and Xy p py a 6 5 a b E B where py is any instance for 2 The binary operation cross denoted by amp performs a parallel product Its set theoretical definition is given by Xaler 2 py ax c b d a b Xy e1 py and c d Xy e2 Pa where e and ez are arbitrary PDOCFA expressions In algebraic terms operation cross is definable with the aid of fork via the equation 7 61 V p e2 e1 e2 By dom e we denote the partial identity over the elements in e s domain Similarly by ran e we denote the partial identity over the elements in e s range In algebraic terms we have e e amp iden dom e and e e amp iden ran e DEFINITION 3 2 8 ran e1 2 if rank e1 1 rank e2 2 m ran e1 e3 p if rank e1 1 rank e2 gt 2 4 dom e1 e2 i
157. y Analyzer we look for an environment that satis fies formula witnessSearch The environment allows us to retrieve a term t that denotes a nonempty set in which all objects satisfy formula alpha This is the witness precandidate In order to prevent the analysis from returning previously discarded terms the model includes a fact that is iter atively enriched in order to prevent previously discarded terms from being produced 4 Dynamite 70 sig A 1 one sig cA extends A sig B f A abstract sig Term complexity Int abstract sig UnaryTerm extends Term unaryValue set univ abstract sig BinaryTerm extends Term binaryValue univ gt univ one sig UnivSyntax extends UnaryTerm unaryValue univ one sig A_ Syntax extends UnaryTerm unaryValue A one sig cA Syntax extends UnaryTerm unaryValue cA one sig B Syntax extends UnaryTerm unaryValue B one sig f Syntax extends BinaryTerm binaryValue f fact sigComplexity A Syntax complexity 1 and cA Syntax complexity 1 and B Syntax complexity 1 and f_Syntax complexity 2 sig UnarySum extends UnaryTerm operandO operandl UnaryTerm H complexity operand0 complexty operand1 complexity 1 unaryValue operand0O unaryValue operand1 unaryValue sig Binarylntersection extends BinaryTerm operandO operand Binary Term H complexity operand0 complexty operand1 complexity 1 binaryValue operandO binaryValue amp operand1 binaryValue
158. y also allows the user to define custom predicates and functions They act as named formulas and expressions that can be reused across the specification For example the following axiom ensures that the directory hierarchy has no loops fun ancestorsp Dir Dir x parent fact NoOwnAncestor all d Dir d lin ancestors d The Alloy language provides support for integer numbers But in order to be able to automatically analyze models the user must provide a bound to the count of integers being referenced in the specification This bound called the bit width is the number of binary digits used to represent integer atoms using 2 s complement arithmetic For instance with 5 as bit width we can represent integers 16 through 15 There is a built in signature Int that denotes the set of all integers up to the user provided bound So integers can appear as atoms in relations For example if we wanted to enrich the directories of our example with the count of elements contained by them we could write sig DetailedDir extends Dir filesCount Int Alloy offers arithmetic operators for addition add substraction sub multiplication mul integer division div and remainder of an integer di vision rem as well as the usual operators for comparison between integers lt lt gt gt All these operators are defined using 2 s complement arithmetic For example 15 1 16 holds when bit width 5 is cho sen Th
159. y idenz which models the set of Alloy integer atoms in the range 2D9e 4 obw 1 determined by the bit width In our theory idenz is a set of urelements and 0 and bw are constants that denote the integer value 0 and the bit width respectively Notice that while 0 is always contained in denz bw may not be when bw 1 2 Therefore we will focus on the general case bw gt 2 and come back to the cases in which bw 1 2 after the presentation of the general case Axiomatically idenz in ideny point 0 point bw 0 in idenz bw in idenz 3 13 We introduce a binary predicate symbol which stands for a linear order with endpoints over idenz In order to simplify the notation quantifications over Z are indeed quan tifications over points contained in idenz For example all a Point a amp amp a in idenz a ala Z o some a Point a amp amp a in idenz amp amp o somea Z a 3 Formal background 42 We will denote by Max x the integer unary predicate some a Z lt a A predicate Min x is symmetrically defined Binary predicate lt is charac terized by the axioms allab Z a bl b aljla b alla Z a lt a alla b c Z a lt b amp amp b lt c Sa lt c some a Z Min a some a Z Max a We next introduce the unary function succ which models the successor function 4 1 according to 2 s complement arithmetic all a b Z Max b amp amp a lt b gt a lt succ a
160. ypothesis iff a some z ones a by Def of E The rest of the cases to be proven can be solved following similar strategies E LEMMA A 0 5 Let be a proper PDOCFA Let p be a relational instance Then there exists an Alloy instance a built according to Def 3 2 6 such that for every Alloy formula y Tr ye W ae Proof The proof proceeds by induction on the structure of formula g e Q ti in ta SP Freee in ta iff SP E E 1 in T te by Def 3 2 12 lt gt p T t1 p T t2 as in previous proof lt a ti alta by Lemma A 0 2 lt a Eti in ta by Def of The remaining parts of the proof follow a structure similar to that of the proof of Lemma A 0 4 7 LEMMA A 0 6 Given an Alloy instance a there exists a proper PDOCFA com patible with a Proof Assume the Alloy model declares signatures Sig Sig Let A Us e Sig Let Tree A be the smallest set satisfying the following conditions e AC Tree A and e Tree A x Tree A C Tree A Tree A describes finite binary trees with data from A in the leaves For in stance element ao a4 a2 a3 as a5 Tree A describes the tree A Complete Proofs of Lemmas from Chapter 3 109 ag a3 A4 a5 Let us consider the PDOCFA with universe Pw Tree A x Tree A All the operators but fork have their standard set theoretical meaning For fork we define RVS a b c a b ER amp amp a c eS In order
161. zi n n2 min if n n2 lt mini n na if mini lt n n2 mazi 1 Sub e mini n n2 maa if n n2 maxi mazi n m2 mini if n n2 lt min e1 mul ez nino mini 4 nana mazi 1 96 2 mi n2 fai mini if n gt 0 and n2 gt 0 1 if ni gt 0 and n2 0 ni n2 maxi if n gt 0 and no lt 0 1 div e2 0 if n 0 ni n max if n lt 0 and no lt 0 1 1 if n lt 0 and n3 0 n1 n2 mini if n lt 0 and n2 gt 0 0 ifn 0 e rem ez ni if n 40and n2 0 n n2 otherwise e sum inte Ne intVal v when E e i 1 veE e i when E ei i 1 Vi 1 lt i lt z sum 21 81 Taie2 e DE intVal v and p E 1 for each i v E e i l etiotz oai M lei E e i i 1 lt i lt z letv e n cal n i v E e i ltv n n cal n i amp v gt int Vat cal n1 i eae cal n 18 v gt O ifi a cal n i otherwise let v4 21 U z n cal let v 21 let v9 22 U c n i In this definition each n stands for the result of cal e i where e is a numeric expression mini maz denotes the minimum maximum integer defined in i Z denotes the number of integer values defined in i note that Z 2 where bw is the so called bit width of the instance Additionally the expression a i b denotes a if min lt a lt maz and b in other case Tab 3 2 Definition of

Biblioteca Digital

Contents

Download Pdf Manuals

Related Search

Related Contents