H-PILoT User Manual Version 1.95
Contents
1. int any non negative number 30 References 1 A R Bradley Z Manna and H B Sipma What s decidable about arrays Proceedings of 7th Int Conf on Verification Model Checking and Abstract Interpretation LNCS vol 3855 2006 Harald Ganzinger Relating semantic and proof theoretic concepts for poly nomial time decidability of uniform word problems Proceedings of the 16th IEEE Symposion on Logic in Computer Science LICS 01 IEEE Comp Soc Press 2001 pp 81 92 S McPeak and G C Necula Data structure specifications via local equality axioms Computer Aided Verification 17th International Conference CAV 2005 LNCS vol 3576 2005 pp 476 490 V Sofronie Stokkermans Hierarchic reasoning in local theory exten sions 20th International Conference on Automated Deduction CADE 20 R Nieuwenhuis ed LNAI no 3632 Springer 2005 pp 219 234 Interpolation in local theory extensions International Joint Con ference on Automated Reasoning IJCAR 2006 U Furbach and Natarajan Shankar eds LNAI no 4130 Springer 2006 pp 235 250 Local reasoning in verification Proceedings of the Verification Workshop VERIFY 06 2006 Hierarchical and modular reasoning in complex theories The case of local theory extensions Proceedings 6th International Symposion on Fron tiers of Combining Systems FroCos 2007 LNCS no 4720 Springer 2007 invited paper pp 47 71 Viorica2. additional_base_clauses constant_list constant additional_constants O BS additional_constants constant additional_constant identifier bool identifier int identifie real identifie scalar q E E identifier pointer C C constant r r identifier pointer int identifier free identifier free int base_clause clausematriz universalQuantifier clausematrix formula_list formula formula additional_formulas additional_formulas e formula additional_formulas clause_list clause clause additional_clauses additional_clauses clause additional_clauses clause clausematriz universalQuantifier clausematria formula OR clausematrix universalQuantifier formula OR clausematriz formula y gt clausematriz universalQuantifier formula gt clausematriz universalQuantifier FORALL variables variables name additional_variable additional_variables e name additional_variables ground_clauses clausematrix ground_clauses clausematrix literal disjunctive_clause sorted_clause formula atom NOT formula OR formula formula_plus AND formula formula_plus formula gt formula formula lt
3. 1 gt 2 G 2 of x lt y gt V x y ATA o gt V x y of x lt y gt M x y x gt y gt M x y of o x Pays ol gt o x x y gt _1 gt o x of gt x lt y gt r x y x gt y gt r x y gt y y gt x 1 r b a _1 14 xr 1 Y X X y y _0 y x y 1 ay 1 x y 4 3 Types In default mode using SPASS H PILoT hands over a set of general first order formulas without types However H PILoT also provides support for the stan dard types int real bool and for free types When using CVC or Yices the default type is int for REDLOG it is real The default type does not need to be specified in the input file You can also use the real flag to set the default type to real for Yices and CVC Free types are specified as free i i 1 2 or simply as free if there is only one free type When using free types the flag freeType must be set Only Yices and CVC are able to handle free types Yices is default When using mixed type in one input file the types of the functions and the constants need to be declared H PILoT does not try to deduce types If the domain of a function is the same as the range it is enough to specify the domain as in foo arity level domainT ype if they differ say foo arity level domainT ype rangeT ype Constants are simply declared as name type We offer the following example taken
4. where the null are of the appropriate type We will call pointer scalar formulas complying with this restriction nullable It was shown in 9 that nullable pointer scalar axioms of the above form are v stably local This result allows the integration of pointer reasoning with the above features into H PILoT As an example cf 3 consider doubly linked lists of decreasing priorities Base_functions 2 2 Extension_functions next 1 1 pointer prev 1 1 pointer priority 1 1 pointer real Relations gt 2 Constants a pointer b pointer Clauses FORALL p prev next p p FORALL p gt next prev p p FORALL p gt q null priority p gt priority next p 17 Query priority a _5 priority b _6 a prev b NOT a null NOT b null H PILoT can be called without any parameters because the keyword pointer is present This will set H PILoT into pointer mode so that it will add all the nullable terms to the axioms and use the specific locality required Because the scalar type is concrete here real H PILoT will use Yices as the prover its default for arithmetic If we want to leave the scalar type abstract we could write something like psiPointers scalar loc Base_functions Extension_functions 1 next 1 1 pointer prev 1 1 pointer priority 1 1 pointer scalar Relations Constants a pointer b pointer c5
5. x could be greater than any element of a x gt alu or thirdly there is a position p l lt p lt u such that a p 1 lt x and x lt alp In the first two cases we put x at the first resp last position of the array In the third case we insert x at position p and shift the other elements to t he right i e a li 1 ali for i gt p We have to take care to cover aberrant cases where the array contains only 1 or 2 elements As input it will look as follows Clauses case 1 FORALL i i l x lt a i gt a i x FORALL i x lt a l 1 lt i i lt u _1 gt a i a i _1 A case 2 FORALL i i u a i lt x gt x lt a l a i _1 x FORALL i a u lt x 1 _1 lt i i lt u gt x lt a l a i _1 a i _1 case 3 FORALL i x lt a u 1 lt i i lt u a i lt x x lt a i _1 gt a i _1 x FORALL i a 1 lt x x lt a u 1 lt i i lt u x lt a i x lt a i _1 gt a i _1 a i FORALL i a 1 lt x x lt a u i u _1 gt a i a i _1 FORALL i a 1 lt x x lt a u 1 _1 lt i i lt u ali _1 lt x gt a i _1 a i _1 FORALL i j 1 lt i i lt j j lt u gt a i lt a j with the last clause saying that a was sorted at the beginning There are several things to note Most importantly we now have a two step extension Firs
6. Our query will usually be denoted by G That is we want to know whether To U K GEL 1G may contain new constants In this case we want to show that cy lt cy lt dy Aca lt dy Ada lt 3 Ada lt ca A f di lt g d2 implies f co lt g c4 Expressed as a satisfiability problem this gives us the following query G co lt c1 lt di c lt di do lt c3 Ada lt c4 A f di lt g d2 A f co lt glca As an input file for H PILoT this looks as follows we use R as order relation because lt is reserved Two monotone functions over a poset Status unsatisfiable Base_functions Extension_functions f 1 g 1 Relations R 2 R is partial order Base FORALL x R x x FORALL x y z R x y Rly z gt R x z FORALL x y Rix yl Rly x gt x y Clauses FORALL x y R x y gt R If x fly FORALL x y R x y gt R g x g y Query R cO c1 R c1 di R c2 di R d2 c3 R d2 c4 R f d1 g d2 NOT R cO0 g c4 In this case we have no function symbols at all in our base theory and two functions symbols f and g of arity 1 in our extension clauses This is expressed by Base_functions Extension_functions f 1 g 1 We have only one relation in our base clauses viz R It has arity 2 of course This we express by Relations R 2 Relations require square brackets as seen above The symb
7. Sofronie Stokkermans and Carsten Ihlemann Automated reasoning in some local extensions of ordered structures Proceedings of ISMVL 2007 IEEE Computer Society 2007 http dx doi org 10 1109 ISMVL 2007 10 Viorica Sofronie Stokkermans Swen Jacobs and Carsten Ihlemann On lo cal reasoning in verification Proceedings of TACAS 08 LNCS vol 4963 Springer 2008 pp 265 281 31
8. an example consider the case of multiple valued logic 8 The class MY of all MV algebras is the quasi variety generated by the real unit interval 0 1 with the Lukasiewicz connectives V A 0 ie the algebra 0 1 0 1 V A o Further the Lukasiewicz connectives can be defined in terms of the real and lt giving us a local extension over the real unit interval Therefore the following are equivalent 1 MYV E YT Na silz ti Z gt s t z 2 0 1 E YZ Aj si ti gt s t 7 3 To UDefr A Aj sie ti A s t c where J consists of the real unit interval 0 1 with the operations and predicate symbol lt For instance we might want to establish that linearity x gt y V y gt x 1 follows from the axioms As an input file for H PILoT it looks like this file mvi loc Example for MV algebras The Lukasiewicz connectives can be defined This feature is not supported for SMT Z3 settings 13 in terms of the real connectives lt Base_functions 2 Extension_functions V 1 Relations lt 2 Interval K Clauses NO Query 0 lt x lt 1 definition FORALL x y FORALL x y definition FORALL x y FORALL x y definition FORALL x y FORALL x y definition FORALL x y FORALL x y linearity x T V r a b lt 2 2 M 1 Co
9. by introducing fresh names for all the extension terms Call these unit clauses D Outside D we only use these new names This gives us a set To Ko Go D where only D contains extension terms now In a final step we eliminate even those by replacing each definition of an extension term by a certain congruence axiom which no longer contains extension functions In this way we have gotten rid of all extension terms and face now a sat isfiability problem over the base theory To Further we need no longer worry about partial models Provided we have an efficient prover for this base theory we have now an efficient way of dealing with a large class of theory extensions H PILoT is a program carrying out this very reduction and handing over to such a prover Let us start with an easy example 3 Examples As a first example let us consider monotone functions over some partially ordered set We consider two monotone functions f and g as extension over the base theory of a partial order That is our base theory consists of the axioms for reflexivity transitivity and anti symmetry 1 Vx x lt x 2 Vi y x lt y y lt x gt y 3 Vx y z x lt yN Ny lt z gt lt z Our extension consists of the two new function symbols together with the clauses expressing monotonicity 1 Vz y x lt y gt f x lt f y 2 Vx y x lt y gt g x lt gly We will always call our base theory To and the extension clauses K
10. from 6 Pointers status unsatisfiable Base_functions 2 2 Extension_functions next 1 1 free 1 prev 1 1 free 1 priority 1 1 free 1 real state 1 1 freettl free 2 Relations gt 2 Constants null free 1 eps real a free 1 b free 1 RUN free 2 WAIT free 2 IDLE free 2 K Clauses FORALL x OR state x RUN state x WAIT state x IDLE prev and next are inverse FORALL p OR p null prev mext p null prev next p p FORALL p gt p null next prev p null next prev p p FORALL p q next q next p gt p null q null p q FORALL p q prev q prev p gt p null q null p q FORALL p gt p null next p null state p IDLE state next p IDLE state p state next p FORALL p OR p null next p null NOT state p RUN priority p gt priority next p 5But recall that they are only able to handle linear arithmetic for reals 15 Query NOT eps 5 NOT eps _6 priority a _5 priority b _6 a prev b state a RUN NOT next a null NOT a null NOT b null 16 4 4 Pointers We consider pointer problems over a two typed language One of which is the type pointer and the other is some scalar type The scalar type can be concrete like real say or kept abstract in which case it is written as scalar In 3 Necula and
11. gt formula FORALL variables formula C EXISTS variables formula 28 formula_plus formula formula_star formula_star formula formula_star disjunctive_clause OR literal literal_plus gt literal_plus literal literal star literaLstar literal literal_star sorted_clause atom_list gt atom_list atom_list atom atom_star atom_star atom atom_star literal atom NOT atom atom equality_atom ineg_atom predicate_atom equality_atom term term ineg_atom term unegs term predicate_atom identifier term additional_terms 1 arguments term additional_terms additional_terms term additional_terms term name a arguments array ae update arguments term_arith arithop term_arith term_arith term_arith name operator arguments C term_arith arithop term_arith C term_arith operator identifier array write identifier term term write array term term update update identifier term term update update term term 29 name identifier identifier any string consisting of letters and numbers starting with a letter It may end with
12. improves readability however Therefore the program will do it for you if you tell it to preprocess the input 4 Advanced features 4 1 Arrays In 1 Bradley Manna and Sipma showed a large fragment of the theory of arrays to be decidable the so called array property fragment This is a 3V fragment of the theory of arrays that imposes syntactical restrictions In a nutshell these restrictions are 1 An Index guard is a positive Boolean combination of atoms of the form t lt u or t u where t and u are either a variable or a ground term of linear arithmetic 2 A universal formula of the form VZ yr Z gt wv is an array property if it is flat if yr is an index guard and if all occurrences of the variables are shielded by extension functions in yy i e variables x only occur as direct array reads a x in py In this section we will only consider extensions by clauses of the above form Our base theory will always be linear integer arithmetic Presburger In the paper 1 it was shown that a limited set of instances is sufficient to decide any query over the fragment This is not quite locality since the set of instances is slightly larger This led us to the generalization of minimal locality see 9 for details In H PILoT minimal locality is also implemented Call hpilot opt arrays k loc to use this feature Let us again consider the example of inserting into a sorted array a Let d be just like a but for p
13. scalar c6 scalar Clauses FORALL p prev next p p FORALL p next prev p p FORALL p NOT priority p priority next p Query priority a cb priority b c6 a prev b c5 c NOT a null NOT b null We again can simply type hpilot opt preprocess psiPointers scalar loc without any parameters H PILoT will again recognize this as a pointer problem and use Yices as default this time because of the free type scalar Pointer extensions can be fused with other types of extensions in a hierarchy However due to the different types of locality that need to be employed the user must specify which levels are pointer extensions He does this by using the keyword Stable For example the header of a more complicated verification task which mixes different pointer types might look like this Base_functions 2 2 Extension_functions 6 Which stands for stable locality which is the type of locality used for pointer extensions 18 level 4 next 1 4 pointer 2 pointer 2 pos 1 4 pointer 2 real level 3 next 1 3 pointer 2 pointer 2 pos 1 3 pointer 2 real spd 1 3 pointer 2 real segm 1 3 pointer 2 pointer 1 level 2 bd 1 2 real real level 1 1max 1 1 pointer 1 real length 1 1 pointer 1 real nexts 1 1 pointer 1 pointer 1 alloc 1 1 pointer 1 int Relations lt 2 gt 2 2 lt 2 Constants t3 pointer 2 t2 poi
14. sorted theories e g lists or arrays with integers as indices and some type of entries Further particularly in recent years very efficient solvers for prominent background theories have been developed e g real number and integers However to take advantage of these one needs to find a way of using these provers as background theory solvers in extended cases Even in the case of extending a theory such as the real numbers with some free uninterpreted functions this is not a trivial task To deal with these types of problems the theory of local theory extensions was developed and H PILoT is an implementation of this approach H PILoT will carry out a reduction and will hand over the transformed problem to a dedicated prover such as Yices or CVC Examples of local extension appearing in verification include e Extensions by free uninterpreted functions e Extensions by monotone functions e Definitional extensions case distinctions e Fragments of the theory of arrays e The theory of pointer structures 2 Background The theory of locality was developed by Harald Ganzinger and Viorica Sofronie Stokkermans 2 4 5 7 The main idea is to limit the search space for counterex amples hence the name Suppose we have a set of universal clauses VK and some ground clause G and we want to check whether VK G or equivalently if VK 7AG L If K is a local set of Horn clauses we need not consider the whole universe of a model but o
15. H PILoT User Manual Version 1 95 Carsten Ihlemann October 21 2010 Abstract H PILoT Hierarchical Proving by Instantiation in Local Theory exten sions is a program that employs hierarchical reasoning for a distinct class of theory extensions It serves as a front end which produces a reduction of a set of clauses to a set of clauses of the base theory and then calls a dedicated solver for the base theory The extensions for which these reductions are possible are called local extensions They include many examples of theories found in real life software verification Contents 1 Introduction 2 Background 3 Examples 4 Advanced features dol ACTAS ei A ge ee G bar ee tl DAZA 4 2 Global constraints 0 0 0 00002 ee ee 43 UV DOSE E hee e ee a Roe Dar AE IE aa aad de 4 elas AA POMC CTS x se L elas A8 eS Bs Bee PE See rp 4 5 Extended locality o oo e 4 0 Clausiticatbion uta sa de bo da e ri a 5 Parameters of H PILoT 6 Error handling 7 The input grammar References 10 10 12 14 16 19 21 23 25 26 30 1 Introduction H PILoT Hierarchical Proving by Instantiation in Local Theory extensions reduces queries over an extended theory to an equivalent query over the base theory This reduction is always possible in the case of so called local extensions 4 This approach is quite relevant for real life verification tasks where one typically faces queries over a mixed bag of multi
16. L 1 z_1 z_3 _O lt z_1 gt _0 lt delta z_1 z_3 L 0 telling us that the above formula resulted in two new clauses in addition to those outright given under Clauses viz Vz1 23 0 lt delta z1 23 V 0 lt 21 and Vz1 22 23 labs z2 23 lt delta z1 z3 V abs f 22 f 23 lt 21 V 0 lt 21 In this case no ground clause resulted and H PILoT stops 23 5 Parameters of H PILoT H PILoT has several input parameters controlling its behavior They can be listed by calling hpilot opt help min prClauses noProver yices Z3 flatten linearize flattenQuery preprocess noSeparation unPseudofy noProcessing clausification real redlog version freeType Use minimal Locality This is only relevant for the array property fragment right now Produce output print all the clauses calculated and used Do not hand over to prover just produce output Use Yices as background solver arithmetics plus etc are predefined as are the order relations lt gt lt gt Numbers can also be given in the input _i is translated to 1 Numbers are integers by default use real for real numbers Use CVC as background solver Arithmetic is predefined as with yices Use Z3 as background solver Arithmetic is predefined as with yices Flatten clauses first Linearize clauses first Flattens the query first Preprocess input flatte
17. McPeak investigate reasoning about pointers in this two typed language with the additional features that there are only two function types viz pointer pointer and pointer scalar where scalar is either a concrete scalar type e g real or the abstract scalar type H PILoT allows the user to specify multiple pointer types p1 Pn n gt 1 as pointer 1 pointer n or simply as pointer if n 1 There are two types of pointer functions Functions Xi of signature p gt p from one pointer type to another and functions X of signature p gt s from a pointer type into scalars A constant null of sort p exists for each i 1 lt i lt n The only predicate of sort pj 1 lt lt n is equality predicates of sort s are allowed and can have any arity The axioms considered are all of the form Vp EVC where p is a set of pointer variables containing all the pointer variables occurring in E VC E contains disjunctions of pointer equalities and C is a disjunction of scalar constraints i e literals of scalar type V C may also contain free variables of scalar type or equivalently free scalar constants In order to rule out null pointer errors Necula and McPeak demanded that pointer terms appearing below a function should not be null That is for all pointer terms fi fo fn p Ji XP UES i 1 n occurring in the axiom the axiom also contains the disjunction p null V fn p null y V V fal fa p null
18. ations lt 2 K Clauses FORALL i j _O lt i i lt j write write a k w l x FORALL i j _O lt i i lt j write write a k y l z Query w _1 lt x x _1 lt y yY _1 lt z _0 _1 lt k k _1 lt l 1 _1 lt n k _3 lt l E 2 12 n _1 gt write write a k w 1 x j n _1 gt write write a k y 1 z j As above H PILoT will also automatically split on disequations in the an tecedent Note also that since we assume that indices of arrays are integers it makes no difference whether we write w _1 or plus w _1 in the input file Linear integer arithmetic will be used Yices is default 4 2 Global constraints Sometimes we want to restrict the domain of the problem e g we want to consider natural numbers instead of integers or we are interested in a real interval a b only Yices and CVC support the definition of subtypes When using one of these it is possible to state a global constraint on the domain of the models in the preamble like thus Interval 0 lt x lt 1 This will restrict the domain of the models of the theory to the unit interval 0 1 It is equivalent to adding the antecedent 0 lt x lt 1 for every variable x to each formula in the clauses and the query The bounds of the interval can also be exclusive or mixed as in Interval O lt x lt 1 or one sided as in Interval 2 lt x As
19. irements index guards must be positive We must rewrite K in a suitable fashion We change an expression 4 l where i is the universally quantified variable to lt J 1VI 1 lt i We have to rewrite it like this because the universally quantified variable i 11 must appear unshielded in the index guard This gives us the following set of clauses Vi J 0 lt lt j lt n 1 gt cli lt elj Vi J 0 lt lt j lt n 1 gt eli lt e j vi i lt 1 1 gt bli c i Vi 1 1 lt gt bli c i Vi i lt k 1 gt ali b i Vi k 1 lt gt ali b i vi i lt 1 1 dfi e i Vi 1 lt gt dfi e i vi i lt k 1 ali dli Vi k 1 lt gt ali dli Ae O N e a A E AI SSF Se Nt iciaih K KH AAA AAA A A A A O ON al o Also K is not linear this must also be taken care of H PILoT will carry out all these necessary rewrite steps for the user He can simply input the above file to deal with this example You can also use a write function when specifying array problems For example use write a i 2 to denote a new array which is just like a except possibly at position where the value of the new array is set to x In this way we could have specified our problem above as Arrays for minimal locality with write function Base_functions 2 Extension_functions a 1 Rel
20. n linearize clauses flatten query In array context split clauses which contain inequalities like i Z j into two clauses Stop at calculating instances K G Don t introduce names for extension terms and don t reduce to base theory See 4 for background Eliminate pseudo quantifiers like Vi 2 3 before handing over to a prover No computation Just translate into prover syntax and hand over Overrides preprocess and turns off clausification When using this flag one should provide the domains of functions too When used in combination with CVC there may arise problems with boolean types true false Turns clausification of general formulas on or off The default is true Implies noProcessing Use real instead of integer linear arithmetic as the default type Call Redlog for base prover Assumes real Print version number Enables the use of an unspecified type free in addition to real and int Only CVC Z3 and Yices accept free types Yices is default 9This is automatically carried out if we have a multiple step extension This is because the next step can only be carried out if the current step resulted in ground clauses 9This is because CVC only provides booleans as bit vectors of length 1 The type BOOLEAN is the type of formulas 24 arrays model smt isLocal renameSubformulas verbosity Use settings for array This combines prepr
21. nly certain ground instances of K viz those ground instances of K in which each term was already a ground term of K or G Let us denote this set of instances of K by K G A theory then is local if we have for an arbitrary ground Horn clause G that VK GE LS K G G E L The same idea works for theory extensions Here we start with a base theory To and extend it by a set of clauses K K contains new function symbols and possibly new sorts We change the definition of K G slightly We consider again instances of K but now we only care about those subterms which start with an extension function Only of those we demand that they already appear as a ground term in K or G Now the extension To C To UK is called local if we have for each set of ground clauses G that To VK G E 1 amp To K G G E L There is an additional twist however due to the fact that elements of K G need no longer be ground We compensate by considering models with partial functions and weak partial semantics 4 That is by To K G G F L we mean that there is no total model of To with partial extension functions in which all ground subterms of K and G are defined and which satisfies K G UG Not only can we get rid of universal quantifiers in a local theory extension by substituting dedicated instances but we can also carry out a full fledged reduction to the base theory We do this in the following manner First we purify To K G G
22. nter 2 t1 pointer 2 d real State0 int s pointer 1 State1 int Stable 1 3 Note that the type pointer 2 must be declared higher than pointer 1 because pointer 2 refers to pointer 1 but not vice versa Here is an example of a header with multiple pointer types at one level Base_functions 2 2 Extension_functions 1 bd 1 1 real real pointer type 1 1lmax 1 2 pointer 1 real length 1 2 pointertt1 real alloc 1 2 pointer 1 int mexts 1 2 pointer 1 pointer 1 pointer type 2 next 1 2 pointer 2 pointer 2 pos 1 2 pointer 2 real spd 1 2 pointer 2 real segm 1 2 pointer 2 pointer 1 third extension updated functions next 1 3 pointer 2 pointer 2 Relations lt 2 2 gt 2 lt 2 Constants t7 pointer 2 t6 pointer 2 t5 pointer 2 t4 pointer 2 Stable 2 19 4 5 Extended locality For some applications we would like that the extension clauses K were allowed to be more complicated say being inductive V3 instead of universal Consider the following example taken from 9 Consider a parametric number m of processes The priorities associated with the processes non negative real numbers are stored in an array p The states of the process enabled 1 or disabled 0 are stored in an array a At each step only the process with maximal priority is enabled its priority is set to x and the priorities of the waiting proce
23. ocess min and arith it also splits clauses on negative equalities Gives a counter model for satisfiable queries Needs Yices or CVC implies Yices by default Produce SMT LIB output without calling a prover Use this flag true false to tell the program whether all the extensions are local or not In the first case h pilot is a full decision procedure in the latter it will only solve unsatisfiable problems Default is false This matters only if H PILoT cannot derive a contradiction In that case this means that there really is none only if the extensions are local true false Use subformula renaming when clausifying the input in order to avoid exponential growth Default is true Sanity check If this flag is set the query clauses are left out This is meant as a test in order to ensure that the axioms are not inconsistent already on their own This flags determines the verbosity level 0 1 2 in the output gotten from prClauses From taciturn to garrulous Default is 0 25 6 Error handling In case you get a parsing error you can use export OCAMLRUNPARAM p in bash syntax This will give you a walk through of the parsing process This is of great help in localizing syntax errors To turn it back off use export OCAMLRUNPARAM 26 7 The input grammar start base_functions extension_functions relations constants interval baseTheory formulasOrClauses groundform
24. oes not provide the full functionality of FLOTTER but should be quite powerful enough for most applications As a simple example consider the following cnf fol Base_functions delta 2 abs 1 2 Extension_functions f 1 Relations Formulas FORALL eps a x _0 lt eps gt AND _O lt delta eps a abs x a lt delta eps a gt abs f x f a lt eps Query H PILoT will clausify the Formulas for us To see the output let us use hpilot opt preprocess prClauses cnf fol We will see an output like Adding formula FORALL eps a x _0 lt eps gt AND _0 lt delta eps a abs x a lt delta eps a gt abs f x f a lt eps add_formulas We have 1 levels done 0ur base theory is empty Clausifying formulas 1 FORALL z_1 z_3 OR _0 lt delta z_1 z_3 NOT _O lt z_1 1 FORALL z_1 z_2 z_3 OR NOT abs z_2 z_3 lt delta z_1 z_3 abs f z_2 f z_3 lt z_1 NOT _O lt z_1 Yielding 2 new clauses z_1 z_2 z_3 abs z_2 z_3 lt delta z_1 z_3 _O lt z_1 gt abs f z_2 f z_3 lt z_1 L 1 z_1 z_3 _O lt z_1 gt _0 lt delta z_1 z_3 L 0 TIt only provides standard formula renaming and standard Skolemization 22 After rewriting we have as clauses K z_1 z_2 z_3 abs z_2 z_3 lt delta z_1 z_3 _O lt z_i gt abs f z_2 f z_3 lt z_1
25. oks like this Updating of priorities of processes File update_AE loc Base_functions 1 2 2 Extension_functions a 1 2 bool a 1 1 bool p 1 2 real p 1 1 real Relations lt 2 lt 2 gt 2 Constants x real y real K Clauses FORALL i _1 lt i i lt m gt _0 lt p i FORALL i AND _1 lt i i lt m FORALL j AND _1 lt j j lt m NOT j i gt pCi gt p j gt a i _1 20 FORALL i AND _1 lt i i lt m FORALL j AND _1 lt j j lt m NOT j i gt pCi gt p j gt p i x FORALL i AND _1 lt i i lt m NOT FORALL j i AND _1 lt j j lt m NOT j i gt p i gt p j gt a i _0 FORALL i AND _1 lt i i lt m NOT FORALL j AND _1 lt j j lt m NOT j i gt p i gt p j gt p i p i y FORALL i j _1 lt i i lt m _1 lt j j lt m p i p j gt i j Query _1 lt c y gt _0 NOT c d p c p d The curly braces P are required to demarcate the beginning and the end of the base formula 21 4 6 Clausification H PILoT also provides a simple clausifier for ease of use First order formulas can be given as input with the syntax of the above subsection and H PILoT will translate them into clausal normal form CNF The CNF translator d
26. ols lt lt gt and gt are reserved for arithmetic over the integers or over the reals They may be written infix and there are provers Yices CVC that understand arithmetic and orderings We wouldn t have needed to axiomatize lt at all It is already built into Yices and CVC However the above problem is more general It concerns every partial order not only numbers By default H PILoT calls SPASS SPASS has no in built understanding of orderings and thus lt would be just any old symbol For clarity we used the letter R As for the syntax of clauses one should note that each clause must end with a semicolon be in prenex normal form and all names meant to be univer sal variables must be explicitly quantified Every name which is not explicitly quantified will be considered a constant As we can see in our query Query R cO c1 R c1 di R c2 di R d2 c3 R d2 c4 R f d1 g d2 NOT R cO g c4 Note further that because the background theory extension theory and the query must all be clauses we need to break up the conjunction in our original query into a set of unit clauses A non unit clause may be written as above in a sorted manner P1 Hn gt V1 Vx for y1 A A Pn gt Y1 V V Pk Le as an implication with the negated atoms in the antecedent and the positive atoms in the consequent or as an arbitrary disjunctions of literals The name of the in
27. osition k which is w and let e be just like d except maybe at position where we have written x and similarly for c b and a Our set K of extension clauses looks as follows Vi j Vi j O lt t lt j lt n 1 gt eli vi Al gt bli cli Vi k gt ali bli vi Al gt dli eli Vi i Z k gt ali dli cjl eli 0 lt lt j lt n 1 gt cli lt lt ZA Aaa A SAS 2S aD AE E LE Re n Our query with additional constraints is 10 O lt k lt l lt mn k 3 lt 1 cll x G b k w ell z d k y The input file looks just like that with and written prefix Arrays for minimal locality Base_functions plus 2 minus 2 Extension_functions a 1 b 1 c 1 d 1 e 1 Relations lt 2 K Clauses FORALL i j _O lt i i lt j j lt minus n _1 gt c i lt c j FORALL i j _O lt i i lt j j lt minus n _1 gt e i lt e j FORALL i gt i l b i c i FORALL i gt i k a i b i FORALL i gt i l d i e i FORALL i gt i k a i d i Query plus w _1 lt x plus x _1 lt y plus y _1 lt z plus _0 _1 lt k plus k _1 lt 1 plus 1 _1 lt nm plus k _3 lt 1 c 1 x b k w e l z d k y We need to put the requirement that e and c should be sorted in K because G must be ground K does not yet fulfill the syntactic requ
28. put files to H PILoT can be freely chosen although it is customary to have them have the suffix loc We run H PILoT by calling hpilot opt mono_for_poset loc H PILoT will parse the input file carry out the reduction and then will hand over the reduced problem to SPASS using the same name but with the suffix dfg SPASS terminates quickly with the result that a proof exists SPASS beiseite Proof found Problem mono_for_poset dfg SPASS derived 35 clauses backtracked 0 clauses and kept 41 clauses SPASS allocated 496 KBytes SPASS spent 0 00 02 32 on the problem 00 00 00 for the input 00 00 00 for the FLOTTER CNF translation 00 00 00 for inferences 00 00 00 for the backtracking 00 00 10 for the reduction oo0ooo 2In fact the extension clauses might be more general as we will see later meaning that the set of clauses is inconsistent Just what we wanted to show If you would like to see more of the reduction process use the option prClauses For more on the rationale of the reduction please refer to 4 For a more complicated example let us consider an algorithm for inserting an element x into a sorted array a with the bounds and u We want to check that the algorithm is correct i e that the updated array a remains sorted This could be an invariant being checked in a verification task There are three different cases First x could be smaller than any element in a equivalently x lt a l
29. sses are increased by y This can be expressed with the following set of axioms which we denote by Update p p a a Vi 1 lt i lt maA Vi lt j lt m j i gt p i gt p 5 gt a i 1 Vil lt i lt m VI lt j lt m jfi p i gt p 5 gt p i x Vil lt i lt m N Vj 1 lt j lt m j i gt p i gt p j gt a i 0 Vil lt i lt m Vj 1 lt j lt m j i gt p i gt p 3 gt p i p it y where x and y are considered to be parameters We may need to check whether if at the beginning the priority list is injective i e formula Inj p holds Inj p VijA lt i lt mal lt j lt maiAj gt pl Fply then it remains injective after the update i e check whether Inj p Update p p a a N 1 lt c lt m 1 lt d lt m c d p c p d L The problem here is that we need to deal with alternations of quantifiers in the extension To deal with cases like this the notion of locality needs to be ex tended That is exactly what was done 4 7 In extended locality the extension formulas K may now have the form Vz1 tn P X1 Xn V O 1 n where P x1 Xn is an arbitrary first order formula in the base signature with free variables x1 n and C x1 xn is a clause in the extended signature In H PILoT extended locality is also implemented Extended clauses may be either written as YZ P x V C Z or as Yz C x The input file for H PILoT simply lo
30. t an array can be simply seen as a partial function This gives us the first extension To C Ti To here is the theory of indices integers say which we extend by the function a and the axiom for monotonicity of a Now we update a giving us a second extension T2 gt T where our extension clauses Ko are given by the three cases above Of course we need to make sure that the last extension is also local This is easy to establish however because Ko is a definitional extension or case distinction cf 8 A definitional extension is one where extension functions f only appear in the form y z gt f x t 2 with t being a base theory term and the y are mutually exclusive base theory clauses This is the reason that we have written Vii l x lt a i gt a i x instead of the shorter x lt a l gt a l x to ensure that the antecedents of the clauses are all mutually exclusive Now we know that we are dealing with a definitional and therefore local extension Remember that for assessing if T gt Ti is a local extension T is our base theory That T is itself an extension is of no moment We need to tell the program that we are dealing with a chain of extensions instead of a single one We do this by the simple expedient of declaring to which level of the chain an extension function belongs like thus f arity level In our example that would be Extension_functions a 1 2 a 1 1 The program will now automa
31. tically determine the level of an extension clause In our example an extension clause will have level 2 iff a occurs in it and level 1 otherwise level 0 means base clause Also note that numerals names for integers must be preceded by an un derscore such as _1 and that and may be written infix for readability x are the only functions for which this is allowed Our declarations therefore should look like this Base_functions 2 2 Extension_functions a 1 2 a 1 1 Relations lt 2 lt 2 All that is left to do now is add our query the negation of Vi j 1 lt lt j lt u gt a i lt a j to the mix and hand it over The entire file looks like this ai loc Arrays for definitional extensions Base_functions 2 2 Extension_functions a 1 2 a 1 1 Relations lt 2 lt 2 K Clauses case 1 FORALL i i l x lt a i gt a i x FORALL i x lt a l 1 lt i i lt u _1 gt a i a i _1 case 2 3When using SPASS they may also be written infix but nevertheless they are just free functions for SPASS FORALL i i u a i lt x gt x lt a l a i _1 x FORALL i a u lt x 1 _1 lt i i lt u gt x lt a l a i _1 a i _1 case 3 FORALL i x lt a u 1 lt i i lt u a i lt x x lt a i _1 gt a i _1
32. ulas query base_functions Base_functions function_list extension_functions Extension_functions function_list relations Relations relation_list constants e Constants constant_list interval Interval int sm identifier Interval identifier sm int Interval int sm identifier sm int base_theory Base clause_list formulas clauses formulas clauses clauses formulas formulasOrClauses ground_formulas Ground Formulas formula_list query Query ground_clauses formulas Formulas formula_list clauses Clauses clause_list additional_functions function additional_functions relation_list e relation additional_relations function_list function additional_functions additional_relations relation additional_relations relation unegs int identifier int identifier int arithop int arithop int int arithop int identifier int al i nt i int function L int domain f domain bool int real pointer pointer int scalar free free int 27 base_clause_list clause additional_base_clauses additional_base_clauses base_clause
33. x FORALL i a 1 lt x x lt a u 1 lt i i lt u x lt a i x lt a i _1 gt a i _1 a i FORALL i a l lt x x lt a u i u _1 gt a i a i _1 FORALL i a 1 lt x x lt a u 1 _1 lt i i lt u ali _1 lt x gt a i _1 a i _1 FORALL i j 1 lt i i lt j j lt u gt a i lt a j Query 1 lt m m lt n n lt u _1 NOT a m lt a2 n We do not need to declare a base theory here because we will be using Yices and Yices already knows arithmetic We call H PILoT thus hpilot opt yices preprocess ai loc H PILoT will produce a reduction put it in a file name ai ys and pass it over to Yices which will say unsat or sat A note on the flag preprocess Establishing that some extension is local presupposes that the extension clauses K be flat and linear Flatness simply means that we have no nesting of functions Linearity means first that we have no variable occurring twice in any extension term and further that if any variable occurs in two extension terms the terms are the same In this example we have non flat clauses such as FORALL i i u a i lt x gt x lt a l a i _1 x We rectify matters by a flattening operation rewriting the above clause to FORALL i j j i _1 i u a i lt x gt x lt a l a j x This will not affect consistency of any query w r t K It hardly
Download Pdf Manuals
Related Search