User Manual for QFIS – A Verifier for the Theory of
Contents
1. Type Type TypeList Type INTEGER SEQUENCE BOOLEAN The variable naming convention for variables extends to functions a function returning an integer respectively sequence Boolean must have a name suitable for an integer respectively sequence Boolean variable A function with only a declaration is used as uninterpreted If the in clause is supplied the CVC3 file path is included as theory of the function declared qfis performs no check that the theory in path if any is consistent with the func tion declaration There are two other ways to introduce axioms for a declared function Declarations directory You can set a declarations directory where qfis searches for theories for declared functions The declarations directory can be set either by setting the environment variable QFIS_PRELUDE or with the d path flag when calling qfis See the installation instructions above for rec ommend settings for the declarations directory if you don t set it as suggested concatenation and length are also used as uninterpreted For each function declared function fun T1 T2 Tn T qfis will look for a file named declaration_fun_t_t1_t2_ _tn_ cvc in the declarations directory where each ti is 0 if Ti is SEQUENCE 1 if Tiis BOOLEAN and 2 if Ti is INTEGER Axiom declarations AxiomDeclaration QuantifiedFormula Quantifier You can introduce axioms that are translated into CVC3 qfis allows quantifiers2. until Z 0 or R 0 invariant _sorted_M sorted M _sorted_L sorted L sorted_R sorted R _L_smaller M 0 lt L 1 _R_smaller M 0 lt R 1 _size X Y M L R loop end Verification still fails now the errors reported are about the loop invariant clauses L_smaller and R_smaller for which qfis cannot verify consecution in ductiveness This is because the clauses must be evaluated before and after a generic iteration of the loop to verify consecution but M is empty in the first iteration hence M 0 is undefined and L or R is empty after the last iteration of the loop hence L 1 or R 1 is undefined We weaken the two clauses to _L_smaller M gt 0 and L gt 0 M0 lt L 1 R_smaller M gt 0 and R gt 0 gt M0 lt R 1 qfis can verify the latest version correctly gt qfis merge_sort qfis This is QFIS a verifier for the theory of quantifier free integer sequences 2 routines 2 verified O errors A final consistency check is the smoke test which tries to see if the axioms of sorted and the background theories used are consistent i e False cannot be inferred gt qfis s merge_sort qfis This is QFIS a verifier for the theory of quantifier free integer sequences Smoke test successful the axioms and the background theories seem consistent 12 7 Command line options The help screen of qfis is the following This is QFIS a verifier for t
3. in axioms but not in annotation formulas The syntax for axioms is then een axiom QuantifiedFormula Formula Quantifier VariableDeclaration QuantifiedFormula forall exist where quantifier free formulas are defined as Formula Connective AtomicFormula BooleanQuery SequenceComparison ArithmeticComparison Sequence Subrange Integer IntegerConstant Digit ElementSelection ArithmeticCompound Operator IdentifierList Identifier ii ji io ii 1i li ii ij AtomicFormula Formula not Formula Formula Connective Formula and or 4 gt True False BooleanQuery BooleanIdentifier old BooleanIdentifier BooleanIdentifier IdentifierList Sequence SequenceComparison Sequence Integer ArithmeticComparison Integer A1 lt l lt l gt l2 Sequenceldentifier old Sequenceldentifier Sequenceldentifier IdentifierList e Integer Sequence Sequence o Sequence Subrange Sequence lt Integer Integer gt IntegerConstant ElementSelection Integerldentifier old IntegerIdentifier IntegerIdentifier IdentifierList Sequence ArithmeticCompound Digit O 1 9 Sequenceldentifier IntegerConstant Sequence IntegerConstant Integer Operator Integer pel eee a Identifier Identifier IdentifierList IntegerIdentifier Sequenceldentifier BooleanIdentifier Notice that integer functions use square rather than round brackets to list ac
4. o cons h cat t o TC1 VY i IntList cat nil 1 l VY i IntList cat 1 nil l TC2 VY a y 2 IntList cat 2 cat y z cat cat 2 y 2 TC3 Tarski s editor axiom VY a y u v IntList cat a y cat u v gt I w IntList cat a w u Acat w v y V cat u w z Acat w y v TCA 6 VY a y IntList cat x y z y nil VY a y IntList cat x y y z nil V x y IntList cat x y nil gt nil Ay nil 5 2 Length Length has signature length IntList NONNEGATIVE_INT and the usual inductive definition where NONNEGATIVE INT are the nonnegative integers and congruence relation with respect to concatenation VY i IntList length l 0 amp l nil YV i IntList 1 Anil gt length l 1 length tail l V x y IntList length cat x y length x length y 5 3 Element selection For every element selection A p with p gt 0 appearing in the qfis formulas the translation defines a position function atp IntList INT with the axioms V a IntList T x p gt atp x head tail 1 z VY a y IntList T x p gt at2 cat x y at2 x For each integer a b such that a b p a gt 0 b gt 0 V a y IntList T x a A tail x nil AT y b gt at2 cat 2 y atb y T a p is a shorthand for the formula denoting x has at least p elements ep x nil p 1 i X tail 2 nil AT 2
5. p 1 p gt 1 and tail denotes the function tail applied n times and tail x is just 2 For every element selection A p with p lt O appearing in the qfis formulas the translation defines a position function at_bottomg IntList INT where q p with the axioms V a IntList T z q 1 A tail x nil gt at_bottom x head z V x IntList T z 2 gt at_bottomq x at_bottoma tail x 5 4 Subranges For every subrange Aa b gt with 1 lt a lt b appearing in the qfis formulas the translation defines a function rangea_b IntList IntList with the axioms V a IntList A x b gt rangea_b z nil V a IntList T x b gt rangea_b x II a a b A x p is a shorthand for the formula denoting x has less than p elements NCCT xz nil p l1 en A z p 1 V tail 1 2 nil p gt 1 I x p q is a term corresponding to the subrange from p to q constructed over the list datatype nm cons head tail z nil p q T Sia cons head tail z II p 1 g p lt q For every subrange Aa b gt with 0 gt a gt b appearing in the qfis formu las the translation defines a function range_bottomp_gq IntList IntList where p a q b with the axioms gt range_bottomp_q x nil VY a IntList A x g 1 1 Atail z nil VY a IntList T z q gt range_bottomp_q x I x 1 q p 2 gt range_bottomp_q z range_bottomp_q tail x V x In
6. the program path This version of qfis was tested with CVC3 v 2 2 To install CVC3 under a Debian based distribution you can type sudo apt get install cvc3 If you use Emacs you may want to install the package cvc3 el as well To have syntax highlighting with any text editor supporting GTK source view such as gedit copy the file qfis lang in the directory grammar to the appropriate directory For Ubuntu and other similar distributions sudo cp qfis lang usr share gtksourceview 2 0 language specs 3 Input language qfis s input language includes both a simple modular imperative language to describe computations on sequences of integer variables and an annotation lan guage very close to the quantifier free theory of integer sequences 2 In the following BNF grammars the meta characters are rule defini tion alternative optional part square and round brackets and all other special characters are terminals denotes one or more repetitions 3 1 Differences with the theory of sequences There are some differences between the theory of integer sequences as defined in 2 and the formulas allowed in qfis The major differences are the following e The following table summarizes the way operators on sequences are en coded in ASCII in qfis This manual uses whenever possible pretty print ing but input files must use the ASCII encoding DESCRIPTION NATIVE ASCII PRETTY PRINTED Con
7. USER MANUAL FOR QFIS A Verifier for the Theory of Quantifier Free Integer Sequences Carlo A Furia caf inf ethz ch v 1 1 December 2012 1 What is qfis qfis also QFIS is a static program verifier for imperative programs working on sequences of integers and annotated with formulas in the quantifier free fragment of the theory of integer sequences qfis generates verification conditions from an annotated program by backward reasoning The verification conditions are translated into SMT input files and CVC3 tries to discharge them qfis reports the results of verification back to users If you are familiar with program verifiers such as Boogie 4 5 or Why IB using qfis is a very similar experience except that qfis does not work on generic programs and first order annotations but is targeted to the theory of quantifier free integer sequences described in 2 You can try out qfis online without installing any software through COMCOM at http cloudstudio ethz ch comcom QFIS 2 Downloading and installing qfis is implemented in Eiffel and available for download in source and pre compiled form from http bitbucket org caf qfis Since version 1 1 qfis works on both GNU Linux and Windows environments It is distributed under GNU GPL v 3 or later versions After you have downloaded it you can install qfis following these simple instructions which use Unix shell syntax and commands by default 1 Move the downloa
8. catenation o o Sequence equality Sequence inequality x x Implication gt gt Iff lt lt gt Element selection S 3 3 53 Subrange 5 3 0 S lt lt 3 0 gt gt SK3 02 gt True False ieee True False True False Ranges with mixed endpoints negative and positive or empty interval e g S 2 1 are currently not supported In a range or element selection 1 denotes the first element 2 the second 0 denotes the last element 1 the second to last etc e Regular expressions are currently disallowed in qfis e Arithmetic is not applicable directly to sequences in qfis but only to singletons which are handled as integers In practice this means that every sequence appearing in an arithmetic operation or relation must be projected e g X 1 2 lt Y 1 instead of X 2 lt Y In this respect notice that the empty sequence is not treated as zero and not accepted at all in arithmetic expressions e qfis annotations allow for full integer arithmetic including multiplication and integer division and comparison and other operations between two integer variables For example you can specify that two sequences have the same length e qfis axioms also allow for quantifiers The extensions beyond the quantifier free fragment entail that the resulting verification conditions are in general undecidable unlike the original theory 2 Overall this seemed a better trade off for users given that the underly
9. ded package e g qfis tgz to a directory of your choice e g home user tools mv qfis tgz home user tools The first release was v 0 1 on 24 March 2011 Move to the installation directory and unpack the package cd home user tools gzip cd gqfis tgz tar xvf Unpacking will create a directory e g home user tools qfis with examples prelude files and a binary for your architecture If you want to compile qfis you can get the sources from the same repos itory you have to install the EiffelStudio compiler See the instructions on http www eiffel com qfis has been developed and compiled with EiffelStudio 7 0 To compile the binary launch the script build linux sh or build windows bat according to your platform in the installation directory You may have to edit qfis ecf if the compiler can t locate the libraries needed Add the path to the bin directory to the environment variable PATH ZPATHY in Windows environments export PATH PATH home user tools qfis bin Set the environment variable QFIS_PRELUDE QFIS_PRELUDE in Win dows environment to the prelude directory export QFIS_PRELUDE home user tools qfis prelude Notice that the path stored by the environment variable must use forward slashes even in Windows environments If you don t set the variable qfis will look for background theories in its working directory Install CVC3 and make sure it is reachable from
10. he WHY verification tool 2009 Version 2 18 http proval lri fr 2 Carlo A Furia What s decidable about sequences In Ahmed Bouajjani and Wei Ngan Chin editors Proceedings of the 8th International Sympo sium on Automated Technology for Verification and Analysis ATVA 10 volume 6252 of Lecture Notes in Computer Science pages 128 142 Springer September 2010 3 Claude March Jean Christophe Filliatre The Why Krakatoa Caduceus platform for deductive program verification In Werner Damm and Hol ger Hermanns editors Proceedings of the 19th International Conference on Computer Aided Verification CAV 07 volume 4590 of Lecture Notes in Computer Science pages 173 177 Springer 2007 4 K Rustan M Leino This is Boogie 2 Manuscript KRML 178 2008 5 K Rustan M Leino Specification and verification of object oriented soft ware Marktoberdorf International Summer School 2008 lecture notes 13
11. he theory of quantifier free integer sequences Usage qfis options lt input_file gt where options is one or more of the following h display this notice s perform a smoke test consistency of the axioms w lt wdir gt set lt wdir gt as the work directory default current dir d lt ddir gt set lt ddir gt as the declarations directory default home user tools qfis prelude QFIS_PRELUDE is set t N give up after N seconds for each verification condition default 10 v parse and typecheck only no verification Notice that the declarations directory is set as recommended in the installation instructions We already showed the smoke test feature in the tutorial example Work directory The work directory is where qfis stores the generated CVC3 input files The files are not removed after verification so that you can inspect them for lower level debugging or to see exactly the problem with a failed verification attempt Timeout The timeout is important for non trivial verifications because qfis treats a timed out run of CVC3 as a failed verification This is consistent with the observation that CVC3 is usually rather efficient to determine validity but it often saturates all the available memory when trying to establish Invalid or Unknown If you go for complex verification conditions you may have to give CVC3 some more time to try to prove validity References 1 Jean Christophe Filliatre T
12. ing SMT solving technology includes on the one hand several optimization that introduce incompleteness but works reasonably well on the other hand to prove the validity of formulas as opposed to finding out for sure that they are invalid 3 2 Variable naming qfis is case sensitive Every identifier starts with a letter followed by letters digits or the special characters _ and In addition variables must be named according to the following convention Integer variables identifier starts with lowercase letter Sequence variables identifier starts with uppercase letter Boolean variables identifier ends with the extra character Labels of assertions identifier starts with the extra character _ and ends with the extra character Variables are declared with the following syntax VariableDeclaration Declaration Declaration VariableDeclaration Declaration IntegerlIdentifierList INTEGER SequenceldentifierList SEQUENCE BooleanIdentifierList BOOLEAN IntegerIdentifierList SequenceldentifierList and BooleanIdentifierList are comma separated non empty lists of integer sequence and Boolean identifiers respectively 3 3 Declarations and background theories Annotations can mention logic functions Every logic function must be declared the signature lists the function argument s types according to the syntax FunctionDeclaration Identifier TypeList Type in path TypeList
13. la ClauseList Label Formula RoutineCall call IdentifierList Routineldentifier IdentifierList Compound Instruction Instruction Compound 3 5 Routines Each routine has a signature with input and output arguments and optionally a precondition a postcondition a declaration of local variables a frame The input arguments are assumed read only Pre and postconditions must mention only input and arguments variables or global variables Global variables that may be modified by the routine must be listed in its frame modify RoutineDeclaration routine Routineldentifier Signature Declarations Signature VariableDeclaration VariableDeclaration Declarations Precondition Modify Locals Body Postcondition end Precondition require ClauseList Postcondition ensure ClauseList Modify modify IdentifierList Locals local VariableDeclaration Body do Compound A qfis input file consists of declarations of functions axioms global variables and routines Program ProgramElementt ProgramElement FunctionDeclaration AxiomDeclaration GlobalDeclaration RoutineDeclaration GlobalDeclaration global VariableDeclaration 4 VC generation qfis uses a weakest precondition calculus defined on primitive instructions as follows where a gt y is with every occurrence of x replaced by y and v is a fresh variable of the same type as v skip a
14. llows Let X1 Xn be the global variables mentioned in foo s postcondition with the old syntax In the generation of verification con ditions we prepend some assignments to the routine body that store the old values of X1 Xn in fresh local variables Old_Xj Old_Xn SaveOld Old_X X Old_X Xn NDR WN FH NOOR WMH Then a reference old X to any such variable in the postcondition becomes a reference to the alias local variable Old_X PostOld Postlold Xj old X gt Old_X Old_X Correspondingly we have the following rules VC routine foo require Pre do Body ensure Post end VC Body PostOld U Pre gt wp SaveOld Body PostOld VC A B VC B 6 U VC A wp B 4 VC until F invariant I loop L end I and not F gt wp L J U I and F gt VC until lt gt invariant J loop L end U wo L D U 19 and for all other instructions Inst VC Inst 0 5 CVC3 axiomatization qfis maps integer sequences to Lisp like lists in CVC3 DATATYPE IntList nil cons head INT tail IntList END The singleton sequence n for an integer term n becomes cons n nil 5 1 Concatenation Concatenation is the function cat IntList IntList IntList with the fol lowing axioms Tarski s editor axioms is needed only in the most complex in ference hence commented out for efficiency by default Congruence VY h INT t o IntList cat cons h t
15. nd sequence s first elements are sorted axiom sorted e axiom forall i INTEGER sorted 1 axiom forall L SEQUENCE L gt 1 sorted L lt gt L 1 lt L 2 and sorted L lt 2 0 gt axiom forall X Y SEQUENCE X gt 0 and Y gt 0 gt sorted X and sorted Y and sorted X 0 o Y 1 lt gt sorted X oY Now let us add a basic implementation of merge_sort If the input has zero or one element it is already sorted Otherwise the algorithm works recursively it splits the input into two sequences sorts each sequence and then merges the result Notice that the way the input is split into two subsequences is not relevant for partial correctness but only for progress and performance 10 routine merge_sort A SEQUENCE Result SEQUENCE local L R SEQUENCE do if A lt 1 then Result A else split A into L R call L merge_sort L call R merge_sort R call Result merge L R end ensure _sorted sorted Result _same_size A Result end merge takes two sorted sequences and returns a merged sorted sequence routine merge X Y SEQUENCE M SEQUENCE require _sorted_X sorted X _sorted_Y sorted Y do ensure _sorted sorted M same_size M X Y end Calling qfis on the current program results in a successful verification of merge_sort and a failed verification of merge whose implementation we haven t provided yet qfis stops at the fir
16. ssert F F and wp wp wp assume F F gt wp havoc V V V wlx E 6 XH E eA UUN The weakest preconditions of compound and derived instructions is as fol lows wp A B wp A wp B wp split S into 1 Sm Q wp havoc 4 Sm assume S Sj 0 Sm Q wp if F then T else E end F gt wp T and not F gt wp E wp if lt gt then T else E end wp T and wp E wp until F invariant I loop L end I NDR WN FH If a loop invariant is not specified assume J True For routine calls assume foo has m input arguments A Am n output arguments B B precondition Pre True if not specified postcondition Post True if not specified and frame G1 Gn Then the weakest precon dition for a call to foo uses fresh variables for the output arguments to handle the cases where some input and output actuals coincide and saves the value of global variables before the call in other fresh variables Old_locah reused in every routine call wp call V1 Vn foo Ui Um wp assert Pre Aj Am Ui Um Old_local G Sut Old local Gh havoc Gi Gh assume Post A1 Am Bi Bn old Gi old Gh gt Ui Um Wi Vn Oldlocalh Old_localy V1 3 Va Vn 9 With the weakest precondition we generate the set VC of verification con ditions for foo as fo
17. st postcondition of merge which it cannot establish gt qfis merge_sort qfis This is QFIS a verifier for the theory of quantifier free integer sequences Routine merge_sort verified successfully Routine merge not verified Could not verify VC 2 annotation on line 63 2 routines 1 verified 1 errors Let us go on and provide an implementation of merge at every iteration of the loop the smallest of the elements in L and R initialized to X and Y because input arguments are read only is added at the end of M Finally if any of the two sequences is not empty after the loop it is also added at the end of M routine merge X Y SEQUENCE M SEQUENCE local L R SEQUENCE do L X R Y M e until L 0 or R 0 loop if L 1 gt R 1 then 11 M M oR 1 R RK2 0 gt else M MoL 1 L L K2 0 gt end end if L gt 0 then M M oL else M M oR end end qfis still cannot verify merge because we have provided no loop invariants In particular the first error it encounters Routine merge not verified Could not verify closing of loop on line 38 annotation on line 55 means that it cannot establish that the loop invariant is strong enough to guar antee the postcondition Let us add a loop invariant M L R are always sorted and additionally the first element of both L and R is no smaller than the last element of M Another clause states the invariance of the combined length of M L and R
18. tList T z q For every subrange A lt a 0 with 1 lt a appearing in the qfis formulas the translation defines a function rangea_0 IntList IntList with the axioms V a IntList A x b gt rangea_O z nil V x IntList T z b gt rangea_O x tail r Finally a subrange A lt a a gt is simply treated as the element selection Afa 6 A tutorial example In this tutorial example we are proving the partial correctness of an implemen tation of MergeSort working on sequences of integers The complete example is available qfis s distribution in the subdirectory examples with several other examples You are welcome to submit your own examples to the author MergeSort takes any integer sequence as input and returns the same sequence sorted In this example we only specify that the output is sorted and that it has the same length as the input Correspondingly we introduce the following declaration in qfis routine merge_sort A SEQUENCE Result SEQUENCE do ensure _sorted sorted Result _same_size A Result end We declare the predicate sorted as a logic function with the right signature function sorted SEQUENCE BOOLEAN We also give sorted the intended semantics with an inductive definition Notice that we should also specify how sorted works on concatenations the concate nation of two sequences is sorted iff both sequences are sorted and the first sequence s last element and the seco
19. tual arguments Operator precedence is as follows o arithmetic operators first x then arithmetic comparisons not and or gt lt gt Im plication is right associative and all other binary operators are left associative The old keyword can only appear in postconditions directly in front of global variable identifiers of any type 3 4 Instructions qfis includes instructions for assignment conditional or nondeterministic branch loop intermediate assertions assert assume nondeterministic shuf fling havoc routine call split is the only non conventional instruction de signed specifically for sequences split S into 1 2 Sn is equivalent to havoc 1 S2 Sn assume S S1 0o82 o oSn Compound instructions sit on multiple line or on the same line separated by a semicolon Similarly multiple loop invariant clauses are either separated by labels or semicolons A condition in a conditional or loop lt gt denotes nondeterministic choice Instruction skip assert Formula assume Formula havoc IdentifierList split Sequence into SequenceldentifierList IntegerIdentifier Integer Sequenceldentifier Sequence BooleanIdentifier Formula Conditional Loop RoutineCall Conditional if Condition then Compound else Compound end Loop until Condition invariant ClauseList loop Compound end Condition Formula lt gt ClauseList Formula ClauseList Formu
Download Pdf Manuals
Related Search