Home

nitpick - Isabelle - Technische Universität München

Contents

1. i e a lasso shaped list with a2 as its stem and a as its cycle In general the list segment within the scope of the THE binder corresponds to the lasso s cycle whereas the segment leading to the binder is the stem A salient property of coinductive datatypes is that two objects are considered equal if and only if they lead to the same observations For example the two lazy lists THE w w LCons a LCons b w LCons a THE w w LCons b LCons a w are identical because both lead to the sequence of observations a b a b or equivalently both encode the infinite list a b a b This concept of equality for coinductive datatypes is called bisimulation and is defined coinductively Internally Nitpick encodes the coinductive bisimilarity predicate as part of the Kodkod problem to ensure that distinct objects lead to different obser vations This precaution is somewhat expensive and often unnecessary so it can be disabled by setting the bisim depth option to 1 The bisimilarity check is then performed after the counterexample has been found to ensure correctness If this after the fact check fails the counterexample is tagged as quasi genuine and Nitpick recommends to try again with bisim depth set to a nonnegative integer The next formula illustrates the need for bisimilarity either as a Kodkod predicate or as an after the fact check to prevent spurious counterexamples lemma vxs LCons a xs y
2. overlord bool false neg no overlord Specifies whether Nitpick should put its temporary files in ISABELLE_ HOME USER which is useful for debugging Nitpick but also unsafe if sev eral instances of the tool are run simultaneously The files are identified by the extensions kki cnf out and err you may safely remove them after Nitpick has run Warning This option is not thread safe Use at your own risks See also debug 85 3 35 5 2 Scope of Search card type int_ seq Specifies the sequence of cardinalities to use for a given type For free types and often also for typedecl d types it usually makes sense to specify cardinalities as a range of the form 1 n See also box 5 2 and mono 5 2 card int seq 1 10 Specifies the default sequence of cardinalities to use This can be over ridden on a per type basis using the card type option described above maz const int seq Specifies the sequence of maximum multiplicities to use for a given co inductive datatype constructor A constructor s multiplicity is the number of distinct values that it can construct Nonsensical values e g maz 2 are silently repaired This option is only available for datatypes equipped with several constructors max int seq Specifies the default sequence of maximum multiplicities to use for co inductive datatype constructors This can be overridden on a per constructor basis using
3. Specifies whether genuine and quasi genuine counterexamples should be given to Isabelle s auto tactic to assess their validity If a genuine counterexample is shown to be spurious the user is kindly asked to send a bug report to the author at blanchette in tum de See also max genuine 85 3 5 5 Regression Testing expect string Specifies the expected outcome which must be one of the following e genuine Nitpick found a genuine counterexample e quasi genuine Nitpick found a quasi genuine counterexample i e a counterexample that is genuine unless it contradicts a miss ing axiom or a dangerous option was used inappropriately e potential Nitpick found a potentially spurious counterexample e none Nitpick found no counterexample 42 unknown Nitpick encountered some problem e g Kodkod ran out of memory Nitpick emits an error if the actual outcome differs from the expected outcome This option is useful for regression testing 5 6 Optimizations sat solver string smart Specifies which SAT solver to use SAT solvers implemented in C or C tend to be faster than their Java counterparts but they can be more difficult to install Also if you set the maz potential 85 3 or max genuine 85 3 option to a value greater than 1 you will need an incremental SAT solver such as MiniSat_JNI recommended or SAT4J The supported solvers are listed below Lingeling_JNT Lingeling is an
4. after the locale s begin keyword To falsify False Nitpick must find a model for the axioms If it finds no model we have an indication that the axioms might be unsatisfiable For Isabelle jEdit users Nitpick provides an automatic mode that can be enabled via the Auto Nitpick option under Plugins gt Plugin Options gt Isabelle gt General In this mode Nitpick is run on every newly entered theorem To run Nitpick you must also make sure that the theory Nitpick is imported this is rarely a problem in practice since it is part of Main The exam ples presented in this manual can be found in Isabelle s src HOL Nitpick_ Examples Manual Nits thy theory The known bugs and limitations at the time of writing are listed in 88 Comments and bug reports concerning either the tool or the manual should be directed to the author at blanchette in tum de Acknowledgment The author would like to thank Mark Summerfield for suggesting several textual improvements 2 Installation Nitpick is part of Isabelle so you do not need to install it It relies on a third party Kodkod front end called Kodkodi which in turn requires a Java virtual machine Both are provided as official Isabelle components To check whether Kodkodi is successfully installed you can try out the ex ample in 83 1 3 First Steps This section introduces Nitpick by presenting small examples If possible you should try out the examples on your workstation You
5. Picking Nits A User s Guide to Nitpick for Isabelle HOL Jasmin Christian Blanchette Institut f r Informatik Technische Universitat M nchen May 25 2015 Contents 1 Introduction 2 Installation 3 First Steps 3 1 3 2 3 3 3 4 3 5 3 6 3 7 3 8 3 9 Propositional Logie 30 e oem om dee RU ee ee RON Type Vana o s saoe are ae ee a ee SY we ER CONSTANTS 2 0 wma eee 3 opc Ges 3 4 doe sean a Sk lerizatioN s s lt 4 oe s EROR eA ee RE ee A Natural Numbers and Integers 2 Inductive Datatypes 22 444 wwe oe os eh ae dex eae ee Typedefs Quotient Types Records Rationals and Reals Inductive and Coinductive Predicates Coinductive Datatypes 222229 2448 e4 404 XE 310 SORA na pechos de otis a st ce oc pd ru ef 21 3 11 Scope Monotonicity du 2a Pu 2 xu P oe Goals amp He Gate Se 29 3 12 Inductive Properties 21 5c Be Pi ee ee POP Pu 25 4 Case Studies 27 4 1 A Context Free Grammar 000 27 42 AA Trees ai Be siecle RoE kB a A a BER EIS A a 29 5 Option Reference 33 5 1 Mode of Operation aooaa AED Bebe BA 34 52 Scope of Searches gena ei a e a aA EE AU EL ERE WS 36 md Qu utp ut Format eenn S 212 2103 2148 28 a e I EHE EA 40 Sub Authentication s s sace Motte erp aena a a a IRE Wd 42 5 5 Regression Testing ooa aaa a 42 Dsl VOPtIMIZAONS aean h e esr etr ve d Ge ae saan Ge las deat a 43 Def Himei 1d a ades d e ee ER EAS ELM n 4T 6 Attribute Refere
6. Nitpick s approach is to consider finite subsets N of nat and maps all numbers N to the undefined value displayed as 7 The type int is handled similarly Internally undefined values lead to a three valued logic Here is an example involving int lemma i j n mzint gt ixn jxm lt ixm j n nitpick Nitpick found a counterexample Free variables 1 0 5 m 1 n 0 Internally Nitpick uses either a unary or a binary representation of numbers The unary representation is more efficient but only suitable for numbers very close to zero By default Nitpick attempts to choose the more appropriate encoding by inspecting the formula at hand This behavior can be overridden by passing either unary_ ints or binary_ ints as option For binary notation the number of bits to use can be specified using the bits option For example nitpick binary ints bits 16 With infinite types we don t always have the luxury of a genuine counter example and must often content ourselves with a potentially spurious one The tedious task of finding out whether the potentially spurious counter example is in fact genuine can be delegated to auto by passing check potential For example lemma Vn Suc n An gt P nitpick card nat 50 check potential Warning The conjecture either trivially holds for the given scopes or lies outside Nitpick s supported fragment Only potentially spurious counterexamples may be found
7. 2 It s hard to see why this is a counterexample To improve readability we will restrict the theorem to nat so that we don t need to look up the value of the op constant to find out which element is smaller than the other In addition we will tell Nitpick to display the value of insort t x using the eval option This gives theorem wf insort nat wf t gt wf insort t z nat nitpick eval insort t x Nitpick found a counterexample Free variables tea NL z 0 Evaluated term insorttx NI11 NOLAA A Nitpick s output reveals that the element 0 was added as a left child of 1 where both nodes have a level of 1 This violates the second AA tree invariant which states that a left child s level must be less than its parent s This shouldn t come as a surprise considering that we commented out the tree rebalancing code Reintroducing the code seems to solve the problem theorem wf insort wf t gt wf insort t x nitpick Nitpick ran out of time after checking 8 of 10 scopes 32 Insertion should transform the set of elements represented by the tree in the obvious way theorem dataset_insort dataset insort t x x U dataset t nitpick Nitpick ran out of time after checking 7 of 10 scopes We could continue like this and sketch a full blown theory of AA trees Once the definitions and main theorems are in place and have been thoroughly tested using Nitpick we could start working on the p
8. Free variables x 0 0 y 0 1 Types nat 0 1 nat x nat boxed 0 0 1 0 my_int 0 0 0 1 The values 0 0 and 0 1 represent the integers 0 and 1 respec tively Other representants would have been possible e g 5 5 and 11 12 If we are going to use my int extensively it pays off to in stall a term postprocessor that converts the pair notation to the standard mathematical notation 13 ML x fun my int postproc _ T Const _ Const _ t1 t2 HOLogic mk_number T snd HOLogic dest_ number t1 snd HOLogic dest_ number t2 my int postprocc _t t j declaration x Nitpick_ Model register_term_ postprocessor Q typ my int my_int_ postproc j Records are handled as datatypes with a single constructor record point Xcoord int Ycoord int lemma Xcoord p point Xcoord q point nitpick show types Nitpick found a counterexample Free variables p Xcoord 1 Ycoord 1 q Xcoord 0 Ycoord 0 Types int 0 1 point Xcoord 0 Ycoord 0 Xcoord 1 Ycoord 1 Finally Nitpick provides rudimentary support for rationals and reals using a similar approach lemma 4 z 3 y real A 1 2 nitpick show types Nitpick found a counterexample Free variables qe y 1 2 Types nat 0 1 2 3 4 5 6 7 iicd 33 9 10 0 1 2 94 453 real 3
9. Nitpick found a potentially spurious counterexample Free variable P False Confirmation by auto The above counterexample is genuine You might wonder why the counterexample is first reported as potentially spurious The root of the problem is that the bound variable in Vn Sucn n ranges over an infinite type If Nitpick finds an n such that Suc n n it evaluates the assumption to False but otherwise it does not know anything about values of n gt card nat and must therefore evaluate the assumption to _ not True Since the assumption can never be satisfied the putative lemma can never be falsified Incidentally if you distrust the so called genuine counterexamples you can enable check_ genuine to verify them as well However be aware that auto will usually fail to prove that the counterexample is genuine or spurious Some conjectures involving elementary number theory make Nitpick look like a giant with feet of clay lemma P Suc nitpick Nitpick found no counterexample On any finite set N Suc is a partial function for example if N 0 1 k then Suc is 0 gt 1 15 2 k _ which evaluates to _ when passed as argument to P As a result P Suc is always The next example is similar lemma P op nat gt nat gt nat nitpick card nat 1 Nitpick found a counterexample Free variable P Ax o CAS _ 0 Az _ 0 0 False nitpick card nat 2 Nitpick found no
10. cardinalities total consts smart bool smart neg partial comsts Specifies whether constants occurring in the problem other than con structors can be assumed to be considered total for the representable values that approximate a datatype This option is highly incomplete it should be used only for problems that do not construct datatype values explicitly Since this option is in rare cases unsound counter examples generated under these conditions are tagged as quasi gen uine datatype sym break int 5 Specifies an upper bound on the number of datatypes for which Nit pick generates symmetry breaking predicates Symmetry breaking can speed up the SAT solver considerably especially for unsatisfiable prob lems but too much of it can slow it down kodkod sym break int 15 Specifies an upper bound on the number of relations for which Kod kod generates symmetry breaking predicates Symmetry breaking can speed up the SAT solver considerably especially for unsatisfiable prob lems but too much of it can slow it down peephole optim bool true neg no peephole optim Specifies whether Nitpick should simplify the generated Kodkod for mulas using a peephole optimizer These optimizations can make a significant difference Unless you are tracking down a bug in Nitpick or distrust the peephole optimizer you should leave this option enabled maz threads int 0 Specifies the maximum number of th
11. cardinality This technique is called boxing and is particularly useful for functions passed as arguments to other functions for high arity functions and for large tuples Under the hood boxing involves wrapping occurrences of the types a x b and a gt b in isomorphic datatypes as can be seen by enabling the debug option To illustrate boxing we consider a formalization of A terms represented using de Bruijn s notation datatype tm Var nat Lam tm App tm tm 21 The lift t k function increments all variables with indices greater than or equal to k by one primrec lift where lift Var j k Var if j lt k then j else j 4 1 lift Lam t k Lam lift t k 4 1 lift App t u k App lift t k lift u k The loose t k predicate returns True if and only if term t has a loose variable with index k or more primrec oose where loose Var j k 3 gt k loose Lam t k loose t Suc k loose App t u k loose t k V loose u k Next the subst c t function applies the substitution c on t primrec subst where subst a Var j o J subst o Lam t Lam subst An case n of 0 gt Var 0 Suc m gt lift o m 1 t subst a App t u App subst a t subst o u A substitution is a function that maps variable indices to terms Observe that c is a function passed as argument and that Nitpick can t optimize it away because the recursive call
12. contains the berkmin executable SAT4J SAT4J is a reasonably efficient solver written in Java that can be used incrementally It is bundled with Kodkodi and requires no further installation or configuration steps Do not attempt to install the official SAT4J packages because their API is incompatible with Kodkod SAT4J Light Variant of SAT4J that is optimized for small problems It can also be used incrementally 44 e smart If sat_ solver is set to smart Nitpick selects the first solver among the above that is recognized by Isabelle If verbose 5 3 is enabled Nitpick displays which SAT solver was chosen batch_ size smart_int smart Specifies the maximum number of Kodkod problems that should be lumped together when invoking Kodkodi Each problem corresponds to one scope Lumping problems together ensures that Kodkodi is launched less often but it makes the verbose output less readable and is sometimes detrimental to performance If batch_ size is set to smart the actual value used is 1 if debug 85 3 is set and 50 otherwise destroy constrs bool true neg dont_destroy_constrs Specifies whether formulas involving co inductive datatype construc tors should be rewritten to use automatically generated discrimina tors and destructors This optimization can drastically reduce the size of the Boolean formulas given to the SAT solver See also debug 5 3 specialize bool true neg dont_ spe
13. efficient solver written in C The JNI Java Native Interface version of Lingeling is bundled with Kodkodi and is precompiled for Linux and Mac OS X It is also available from the Kodkod web site 6 CryptoMiniSat CryptoMiniSat is the winner of the 2010 SAT Race To use CryptoMiniSat set the environment vari able CRYPTOMINISAT HOME to the directory that contains the cryptominisat executable The C sources and executables for CryptoMiniSat are available at http planete inrialpes fr soos CryptoMiniSat2 index php Nitpick has been tested with version 2 51 CryptoMiniSat_ JNI The JNI Java Native Interface version of CryptoMiniSat is bundled with Kodkodi and is precompiled for Linux and Mac OS X It is also available from the Kodkod web site 6 MiniSat MiniSat is an efficient solver written in C To use MiniSat set the environment variable MINISAT_HOME to the di rectory that contains the minisat executable The C sources and executables for MiniSat are available at http minisat se MiniSat html Nitpick has been tested with versions 1 14 and 2 2 Important note for Cygwin users The path must be specified using native Windows syntax Make sure to escape backslashes properly 43 MiniSat JNI The JNI version of MiniSat is bundled with Kod kodi and is precompiled for Linux Mac OS X and Windows Cyg win It is also available from the Kodkod web site 6 Unlike the standard version of MiniSat the JNI versio
14. finish off the subgoals 4 Case Studies As a didactic device the previous section focused mostly on toy formulas whose validity can easily be assessed just by looking at the formula We will now review two somewhat more realistic case studies that are within Nitpick s reach a context free grammar modeled by mutually inductive sets and a functional implementation of AA trees The results presented in this section were produced with the following settings nitpick params maz_potential 0 4 1 A Context Free Grammar Our first case study is taken from section 7 4 in the Isabelle tutorial 5 The following grammar originally due to Hopcroft and Ullman produces all strings with an equal number of a s and b s S e bA aB A a bAA B bS aBB The intuition behind the grammar is that A generates all strings with one more a than b s and B generates all strings with one more 5 than a s The alphabet consists exclusively of a s and b s datatype alphabet a b Strings over the alphabet are represented by alphabet lists Nonterminals in the grammar become sets of strings The production rules presented above can be expressed as a mutually inductive definition inductive set 5 and A and B where R1 e S R2 w A b wes 27 R3 we B a wes R4 w E S adi wA R5 w E S gt b we S R6 v B v B a vQweB The conversion of the grammar into the in
15. for the Lam case involves an altered version Also notice the lift call which increments the variable indices when moving under a Lam A reasonable property to expect of substitution is that it should leave closed terms unchanged Alas even this simple property does not hold lemma loose t 0 substo t t nitpick verbose Trying 10 scopes card nat 1 card tm 1 and card nat gt tm 1 card nat 2 card tm 2 and card nat tm 2 card nat 10 card tm 10 and card nat tm 10 Nitpick found a counterexample for card nat 6 card tm 6 and card nat tm 6 22 Free variables o Ax _ 0 Var 0 1 Var 0 2 Var 0 3 Var 0 4 Var 0 5 Lam Lam Var 0 t Lam Lam Var 1 Total time 3 08 s Using eval we find out that subst c t Lam Lam Var 0 Using the traditional A calculus notation f is Az y x whereas subst co t is wrongly Az y y The bug is in subst The lift c m 1 call should be replaced with lift o m 0 An interesting aspect of Nitpick s verbose output is that it assigned inceasing cardinalities from 1 to 10 to the type nat tm of the higher order argument c of subst For the formula of interest knowing 6 values of that type was enough to find the counterexample Without boxing 6 46 656 values must be considered a hopeless undertaking nitpick dont boz Nitpick ran out of time after checking 3 of 10 scopes Boxing c
16. founded The option can take the following values e true Tentatively treat the co inductive predicate as if it were well founded Since this is generally not sound when the predi cate is not well founded the counterexamples are tagged as quasi genuine e false Treat the co inductive predicate as if it were not well founded The predicate is then unrolled as prescribed by the star linear preds iter const and iter options e smart Iry to prove that the inductive predicate is well founded using Isabelle s lezicographic order and size change tactics If this succeeds or the predicate occurs with an appropriate polarity in the formula to falsify use an efficient fixed point equation as specification of the predicate otherwise unroll the predicates according to the iter const and iter options See also iter 85 2 star linear preds 85 6 and tac timeout 85 7 wf smart bool smart neg non wf Specifies the default wellfoundedness setting to use This can be over ridden on a per predicate basis using the wf const option above iter const int seq Specifies the sequence of iteration counts to use when unrolling a given co inductive predicate By default unrolling is applied for inductive 37 predicates that occur negatively and coinductive predicates that occur positively in the formula to falsify and that cannot be proved to be well founded but this behavior is influenced by the wf option
17. occurrences of non well founded linear inductive predicates i e inductive predicates for which each the predicate occurs in at most one assumption of each introduction rule For example inductive odd where odd 1 Dodd m even n gt odd m n lemma odd n gt odd n 2 nitpick card nat 4 show consts Nitpick found a counterexample Free variable n 1 Constants even Ax _ 0 True 1 False 2 True 3 False oddbase m Ax _ 0 False 1 True 2 False 3 False oddstep Ax _ 0 Ax _ 0 True 1 False 2 True 3 False I Ax _ 0 False 1 True 2 False 3 True 2 Ax _ 0 False 1 False 2 True 3 False 3 Ax _ 0 False 1 False 2 False 3 True odd lt Ax _ 0 False 1 True 2 False 3 True In the output oddpase represents the base elements and oddstep is a transition relation that computes new elements from known ones The set odd consists 18 of all the values reachable through the reflexive transitive closure of oddstep starting with any element from oddpase namely 1 and 3 Using Kodkod s transitive closure to encode linear predicates is normally either more thorough or more efficient than unrolling depending on the value of iter but you can disable it by passing the dont star linear preds option 3 9 Coinductive Datatypes A coinductive datatype is similar to an
18. registering and unregistering coinductive datatypes consists of the following pair of functions defined in the Nitpick_ HOL structure 51 val register codatatype morphism typ string string x typ list Context generic Context generic val unregister codatatype morphism typ Context generic Context generic The type a llist of lazy lists is already registered had it not been you could have told Nitpick about it by adding the following line to your theory file declaration x Nitpick HOL register codatatype typ a llist const name llist case map dest_ Const term LNil term LCons j The register codatatype function takes a coinductive datatype its case func tion and the list of its constructors in addition to the current morphism and generic proof context The case function must take its arguments in the order that the constructors are listed If no case function with the correct signature is available simply pass the empty string On the other hand if your goal is to cripple Nitpick add the following line to your theory file and try to check a few conjectures about lazy lists declaration x Nitpick HOL unregister codatatype Q typ a llist j Inductive datatypes can be registered as coinductive datatypes given appro priate coinductive constructors However doing so precludes the use of the inductive constructors Nitpick will generate an error if they are nee
19. type whenever practicable e false Never box the type e smart Box the type only in contexts where it is likely to help For example n tuples where n gt 2 and arguments to higher order functions are good candidates for boxing See also finitize 5 2 verbose 5 3 and debug 5 3 box smart bool smart neg dont box Specifies the default boxing setting to use This can be overridden on a per type basis using the box type option described above 38 finitize type smart_bool neg dont finitize Specifies whether Nitpick should attempt to finitize an infinite data type The option can then take the following values e true Finitize the datatype Since this is unsound counter examples generated under these conditions are tagged as quasi genuine e false Don t attempt to finitize the datatype e smart If the datatype s constructors don t appear in the prob lem perform a monotonicity analysis to detect whether the data type can be soundly finitized otherwise don t finitize it See also box 85 2 mono 5 2 verbose 85 3 and debug 85 3 finitize smart bool smart neg dont finitize Specifies the default finitization setting to use This can be overridden on a per type basis using the finitize type option described above mono type smart bool neg non mono Specifies whether the given type should be considered monotonic when enumerating scopes an
20. 2 1 2 0 1 2 1 2 3 4 14 3 8 Inductive and Coinductive Predicates Inductively defined predicates and sets are particularly problematic for counterexample generators They can make Quickcheck 2 loop forever and Refute 8 run out of resources The crux of the problem is that they are defined using a least fixed point construction Nitpick s philosophy is that not all inductive predicates are equal Consider the even predicate below inductive even where even 0 even n gt even Suc Suc n This predicate enjoys the desirable property of being well founded which means that the introduction rules don t give rise to infinite chains of the form gt even k gt even k gt even k For even this is obvious Any chain ending at k will be of length k 2 1 even 0 gt even 2 gt gt even k 2 gt even k Wellfoundedness is desirable because it enables Nitpick to use a very efficient fixed point computation Moreover Nitpick can prove wellfoundedness of most well founded predicates just as Isabelle s function package usually discharges termination proof obligations automatically Let s try an example lemma dn even n even Suc n nitpick card nat 50 unary_ ints verbose The inductive predicate even was proved well founded Nitpick can compute it efficiently Trying 1 scope card nat 50 Warning The conjecture either trivially holds for the gi
21. The iteration counts are automatically bounded by the cardinality of the predicate s domain See also wf 85 2 and star_linear_preds 85 6 iter int seq 0 1 2 4 8 12 16 20 24 28 Specifies the sequence of iteration counts to use when unrolling co in ductive predicates This can be overridden on a per predicate basis using the iter const option above bisim depth int seq 9 Specifies the sequence of iteration counts to use when unrolling the bisimilarity predicate generated by Nitpick for coinductive datatypes A value of 1 means that no predicate is generated in which case Nit pick performs an after the fact check to see if the known coinductive datatype values are bidissimilar If two values are found to be bisim ilar the counterexample is tagged as quasi genuine The iteration counts are automatically bounded by the sum of the cardinalities of the coinductive datatypes occurring in the formula to falsify box type smart bool neg dont box Specifies whether Nitpick should attempt to wrap box a given func tion or product type in an isomorphic datatype internally Boxing is an effective mean to reduce the search space and speed up Nitpick because the isomorphic datatype is approximated by a subset of the possible function or pair values Like other drastic optimizations it can also prevent the discovery of counterexamples The option can take the following values e true Box the specified
22. a1 a4 hd Ax _ az a1 1 01 61 ai Since hd is undefined in the logic it may be given any value including a The second constant Ax zi y y is simply the append operator whose second argument is fixed to be y y Appending a a1 to a1 would nor mally give ai a a1 but this value is not representable in the subset of a list considered by Nitpick which is shown under the Type heading hence the result is _ Similarly appending a a to itself gives Given card a 3 and card a list 3 Nitpick considers the following subsets 11 V a a2 VI a a2 al V a2 as a2 l a a3 5 V a as al V as 1 asl V a2 a3 VI a2 a a9 as a2 a3 VL a a a V a2 a2 a2 V as las as All subterm closed subsets of a list consisting of three values are listed and only those As an example of a non subterm closed subset consider S il ai a1 a2 and observe that a1 ap i e a a2 has ag S asa subterm Here s another m chtegern lemma that Nitpick can refute without a blink lemma length zs 1 length ys 1 gt zs ys nitpick show_ types Nitpick found a counterexample for card a 3 Free variables zs a5 ys a Types nat 0 1 2 a list a ao Because datatypes are approximated using a three valued logic t
23. ame conclusion after a careful inspection of the formula and the relevant definitions nitpick verbose The types a and b passed the monotonicity test Nitpick might be able to skip some scopes Trying 10 scopes card a 1 card b 1 card nat 1 card a x b list 1 card a list 1 and card b list 1 card a 2 card b 2 card nat 2 card a x b list 2 card a list 2 and card b list 2 card a 10 card b 10 card nat 10 card aX b list 10 card a list 10 and card b list 10 Nitpick found a counterexample for card a 5 card b 5 card nat 5 card a b list 5 card a list 5 and card b list 5 Free variables zs a a2 ys b1 bi Total time 1 63 s In theory it should be sufficient to test a single scope nitpick card 10 However this is often less efficient in practice and may lead to overly complex counterexamples If the monotonicity check fails but we believe that the formula is monotonic or we don t mind missing some counterexamples we can pass the mono option To convince yourself that this option is risky simply consider this example from 83 4 24 lemma Jg Vz b g f z u gt Vy a 3s y f r nitpick mono Nitpick found no counterexample nitpick Nitpick found a counterexample for card a 2 and card b 1 It turns out the formula holds if and only i
24. an be enabled or disabled globally or on a per type basis using the box option Nitpick usually performs reasonable choices about which types should be boxed but option tweaking sometimes helps 3 11 Scope Monotonicity The card option together with iter bistm_ depth and maz controls which scopes are actually tested In general to exhaust all models below a certain cardinality bound the number of scopes that Nitpick must consider increases exponentially with the number of type variables and typedecl d types occurring in the formula Given the default cardinality specification of 1 10 no fewer than 10 10000 scopes must be considered for a formula involving a b c and d Fortunately many formulas exhibit a property called scope monotonicity meaning that if the formula is falsifiable for a given scope it is also falsifiable for all larger scopes 4 p 165 Consider the formula lemma length xs length ys gt rev zip zs ys zip xs rev ys 23 where zs is of type a list and ys is of type b list A priori Nitpick would need to consider 1000 scopes to exhaust the specification card 1 10 10 cardinalies for a x 10 cardinalities for b x 10 cardinalities for the datatypes However our intuition tells us that any counterexample found with a small scope would still be a counterexample in a larger scope by simply ignoring the fresh a and b values provided by the larger scope Nitpick comes to the s
25. ates to either True or never False When unrolling a predicate Nitpick tries 0 1 2 4 8 12 16 20 24 and 28 iterations However these numbers are bounded by the cardinality of the predicate s domain With card nat 10 no more than 9 iterations are ever needed to compute the value of a nat predicate You can specify the number of iterations using the iter option as explained in 85 2 In the next formula even occurs both positively and negatively lemma even n 2 gt even n nitpick card nat 10 show consts Nitpick found a counterexample Free variable n 1 Constants Ai even Ax _ 0 Ax _ 0 True 2 True even lt Ax _ 0 True 1 False 2 True 4 True 6 True 8 True Notice the special constraint even lt in the output whose right hand side represents an arbitrary fixed point not necessarily the least one It is 17 used to falsify even n In contrast the unrolled predicate is used to satisfy even n 2 Coinductive predicates are handled dually For example coinductive nats where nats z nat gt nats z lemma nats An n 0 1 2 3 4 nitpick card nat 10 show_consts Nitpick found a counterexample Constants Ai nats Ax _ 0 Az _ 1 Ax _ 2 Ax 1 nats gt Ax _ 3 True 4 False 5 True As a special case Nitpick uses Kodkod s transitive closure operator to en code negative
26. cialize Specifies whether functions invoked with static arguments should be specialized This optimization can drastically reduce the search space especially for higher order functions See also debug 85 3 and show_consts 85 3 star_linear_preds bool true neg dont star linear preds Specifies whether Nitpick should use Kodkod s transitive closure op erator to encode non well founded linear inductive predicates i e inductive predicates for which each the predicate occurs in at most one assumption of each introduction rule Using the reflexive transitive clo sure is in principle equivalent to setting iter to the cardinality of the predicate s domain but it is usually more efficient See also wf 5 2 debug 5 3 and iter 5 2 whack term_ list Specifies a list of atomic terms usually constants but also free and schematic variables that should be taken as being _ unknown This can be useful to reduce the size of the Kodkod problem if you can guess in advance that a constant might not be needed to find a countermodel 45 See also debug 5 3 need term_ list Specifies a list of datatype values normally ground constructor terms that should be part of the subterm closed subsets used to approximate datatypes If you know that a value must necessarily belong to the subset of representable values that approximates a datatype specifying it can speed up the search especially for high
27. cost u In some rare occasions you might want to provide an inductive or coinductive view on top of an existing constant c The easiest way to achieve this is to define a new constant c co inductively Then prove that c equals c and let Nitpick know about it lemma c_alt_ unfold nitpick unfold c c This ensures that Nitpick will substitute c for c and use the co inductive definition 7 Standard ML Interface Nitpick provides a rich Standard ML interface used mainly for internal pur poses and debugging Among the most interesting functions exported by Nitpick are those that let you invoke the tool programmatically and those that let you register and unregister custom term postprocessors as well as coinductive datatypes 7 1 Invoking Nitpick The Nitpick structure offers the following functions for invoking your favorite counterexample generator val pick mits in term Proof state params mode int int int term x term list gt term list gt term string Proof state val pick mits in subgoal Proof state params mode int int string Proof state 50 The return value is a new proof state paired with an outcome string gen uine quasi_ genuine potential none or unknown The params type is a large record that lets you set Nitpick s options The current default options can be retrieved by calling the following function defined in the N
28. counterexample The problem here is that op is total when nat is taken to be 0 but becomes partial as soon as we add 1 because 1 1 0 1 Because numbers are infinite and are approximated using a three valued logic there is usually no need to systematically enumerate domain sizes If Nitpick cannot find a genuine counterexample for card nat k it is very unlikely that one could be found for smaller domains The P op example above is an exception to this principle Nitpick nonetheless enumerates all cardinalities from 1 to 10 for nat mainly because smaller cardinalities are fast to handle 10 and give rise to simpler counterexamples This is explained in more detail in 83 11 3 6 Inductive Datatypes Like natural numbers and integers inductive datatypes with recursive con structors admit no finite models and must be approximated by a subterm closed subset For example using a cardinality of 10 for a list Nitpick looks for all counterexamples that can be built using at most 10 different lists Let s see with an example involving hd which returns the first element of a list and which concatenates two lists lemma hd as y y hd zs nitpick Nitpick found a counterexample for card a 3 Free variables zs Y ay To see why the counterexample is genuine we enable show consts and show_ datatypes Type a list m m ai Constants Az t ly y Az
29. d A relational model finder In O Grumberg and M Huth editors TACAS 2007 volume 4424 of Lecture Notes in Computer Science pages 632 647 Springer Verlag 2007 T Weber SAT Based Finite Model Generation for Higher Order Logic Ph D thesis Dept of Informatics T U M nchen 2008 Wikipedia AA tree http en wikipedia org wiki AA_tree 54
30. d finitizing types If the option is set to smart Nitpick performs a monotonicity check on the type Setting this option to true can reduce the number of scopes tried but it can also diminish the chance of finding a counterexample as demonstrated in 83 11 The option is implicitly set to true for automatic runs See also card 85 2 finitize 85 2 merge type vars 85 2 and verbose 85 3 mono smart bool smart neg non mono Specifies the default monotonicity setting to use This can be overrid den on a per type basis using the mono type option described above merge type vars bool false neg dont merge type vars Specifies whether type variables with the same sort constraints should be merged Setting this option to true can reduce the number of scopes tried and the size of the generated Kodkod formulas but it also dimin ishes the theoretical chance of finding a counterexample See also mono 85 2 39 5 3 Output Format verbose bool false neg quiet Specifies whether the nitpick command should explain what it does This option is useful to determine which scopes are tried or which SAT solver is used This option is implicitly disabled for automatic runs debug bool false neg no_ debug Specifies whether Nitpick should display additional debugging infor mation beyond what verbose already displays Enabling debug also enables verbose and show all behind the scenes The debug
31. ded 8 Known Bugs and Limitations Here are the known bugs and limitations in Nitpick at the time of writing e Underspecified functions defined using the primrec function or nominal primrec packages can lead Nitpick to generate spurious counterexamples for theorems that refer to values for which the func tion is not defined For example primrec prec where prec Suc n n 52 lemma prec 0 undefined nitpick Nitpick found a counterexample for card nat 2 Empty assignment by auto simp prec_ def Such theorems are generally considered bad style because they rely on the internal representation of functions synthesized by Isabelle an implementation detail e Similarly Nitpick might find spurious counterexamples for theorems that rely on the use of the indefinite description operator internally by specification and quot type e Axioms or definitions that restrict the possible values of the undefined constant or other partially specified built in Isabelle constants e g Abs and Hep constants are in general ignored Again such non conservative extensions are generally considered bad style e Nitpick produces spurious counterexamples when invoked after a guess command in a structured proof e Datatypes defined using datatype new and codatatypes defined using codatatype that involve nested co recursion through non co datatypes are not properly supported and may result in spurious counterexamples e T
32. dles entailed by non wellfoundedness we decrease nat s cardi nality to a mere 10 lemma Jn 0 2 4 6 8 even n nitpick card nat 10 verbose show consts The inductive predicate even could not be proved well founded Nit pick might need to unroll it Trying 6 scopes card nat 10 and iter even 0 card nat 10 and iter even 1 card nat 10 and iter even 2 card nat 10 and iter even 4 card nat 10 and iter even 8 16 card nat 10 and iter even 9 Nitpick found a counterexample for card nat 10 and iter even 2 Constant Ai even Ax c Ote Ax _ 0 True 2 True 1 Ax _ 0 True 2 True 4 True 2 Ax _ 0 True 2 True 4 True 6 True 8 True Total time 1 87 s Nitpick s output is very instructive First it tells us that the predicate is unrolled meaning that it is computed iteratively from the empty set Then it lists six scopes specifying different bounds on the numbers of iterations 0 1 2 4 8 and 9 The output also shows how each iteration contributes to even The notation Ai even indicates that the value of the predicate depends on an iteration counter Iteration 0 provides the basis elements 0 and 2 Iteration 1 con tributes 4 2 2 Iteration 2 throws 6 2 4 4 2 and 8 4 4 into the mix Further iterations would not contribute any new elements The predicate even evalu
33. ductive definition was done man ually by Joe Blow an underpaid undergraduate student As a result some errors might have sneaked in Debugging faulty specifications is at the heart of Nitpick s raison d tre A good approach is to state desirable properties of the specification here that S is exactly the set of strings over a b with as many a s as b s and check them with Nitpick If the properties are correctly stated counterexamples will point to bugs in the specification For our grammar example we will proceed in two steps separating the soundness and the completeness of the set S First soundness theorem S_ sound w S length x w x a length y w z b nitpick Nitpick found a counterexample Free variable w b It would seem that b S How could this be An inspection of the introduction rules reveals that the only rule with a right hand side of the form b S that could have introduced b into S is R5 weS gt b wes On closer inspection we can see that this rule is wrong To match the production B bS the second S should be a B We fix the typo and try again nitpick Nitpick found a counterexample Free variable w a a b Some detective work is necessary to find out what went wrong here To get a a b S we need a b B by R3 which in turn can only come from R6 28 lu B v E B a vQwe B Now this formula must be wron
34. e output for high arity functions For example given the variable y a b gt c gt d e gt f g setting format y 3 tells Nitpick to group the last three arguments as if the type had been a b gt c gt d x e x f gt g In general a list of values n ng tells Nitpick to show the last n arguments as an n tuple the previous n _ arguments as an ny tuple and so on arguments that are not accounted for are left alone as if the specification had been 1 1 mj ny A format int_ seq 1 Specifies the default format to use Irrespective of the default format the extra arguments to a Skolem constant corresponding to the outer bound variables are kept separated from the remaining arguments the for arguments of an inductive definitions are kept separated from the remaining arguments and the iteration counter of an unrolled inductive definition is shown alone The default format can be overridden on a per variable or per constant basis using the format term option described above 5 4 Authentication check potential bool false neg trust_ potential Specifies whether potentially spurious counterexamples should be given to Isabelle s auto tactic to assess their validity If a potentially spurious counterexample is shown to be genuine Nitpick displays a message to this effect and terminates See also max potential 85 3 check genuine bool false neg trust_ genuine
35. els This manual assumes throughout that falsify is enabled 34 user axioms smart bool smart neg no user axioms Specifies whether the user defined axioms specified using axiomati zation and axioms should be considered If the option is set to smart Nitpick performs an ad hoc axiom selection based on the constants that occur in the formula to falsify The option is implicitly set to true for automatic runs Warning If the option is set to true Nitpick might nonetheless ignore some polymorphic axioms Counterexamples generated under these conditions are tagged as quasi genuine The debug 85 3 option can be used to find out which axioms were considered See also assms 85 1 and debug 85 3 assms bool true neg no assms Specifies whether the relevant assumptions in structured proofs should be considered The option is implicitly enabled for automatic runs See also user_ axioms 85 1 spy bool false neg dont spy Specifies whether Nitpick should record statistics in ISABELLE_HOME_ USER spy nitpick These statistics can be useful to the developer of Nitpick If you are willing to have your interactions recorded in the name of science please enable this feature and send the statistics file every now and then to the author of this manual blanchette in tum de To change the default value of this option globally set the environment variable NITPICK SPY to yes See also debug 85 3
36. elt k levelu x k level right u k Rebalancing the tree upon insertion and removal of elements is performed by two auxiliary functions called skew and split defined below primrec skew where skew A A skew N x k t u if t AAA k level t then N data t k left t N x k right t u else Nuwktay primrec split where split A N split N x k t u if u Z A k level right u then N data u Suc k N x k t left u right u else Nu Ex wy Performing a skew or a split should have no impact on the set of elements stored in the tree theorem dataset skew split dataset skew t dataset t dataset split t dataset t nitpick Nitpick ran out of time after checking 9 of 10 scopes Furthermore applying skew or split on a well formed tree should not alter the tree theorem wf skew split quf skew t Tag gt split t t nitpick Nitpick found no counterexample 31 Insertion is implemented recursively It preserves the sort order primrec insort where insons ar LINN insort Ny k t u x x splito skew N y k if z lt y then insort t x else t if x gt y then insort u z else u Notice that we deliberately commented out the application of skew and split Let s see if this causes any problems theorem wf insort wf t gt wf insort t x nitpick Nitpick found a counterexample for card a 4 Free variables t WN Qi 1AA T
37. ese rules as the specification of the constant Otherwise if the nitpick psimp set associated with the constant is not empty it uses these rules as the specification of the constant Otherwise if the constant was defined using the ax specification command and the nitpick choice spec set associated with the constant is not empty it uses these theorems as the specification of the constant Otherwise it looks up the definition of the constant If the nitpick unfold set associated with the constant is not empty it uses the latest rule added to the set as the definition of the constant otherwise it uses the actual definition axiom 48 1 If the definition is of the form Clay lam AY Yn Up Af t or Ay Yaw gfp AJ t Nitpick assumes that the definition was made using a co inductive package based on the user specified introduction rules registered in Isabelle s internal Spec Rules table The tool uses the intro duction rules to ascertain whether the definition is well founded and the definition to generate a fixed point equation or an unrolled equation C 3 Lm 2 If the definition is compact enough the constant is unfolded wher ever it appears otherwise it is defined equationally as with the nitpick simp attribute As an illustration consider the inductive definition inductive odd where odd 1 odd n gt odd Suc Suc n By default Nitpick uses the fp based definiti
38. f card a lt card b Although this is rarely advisable the automatic monotonicity checks can be disabled by passing non_mono 5 6 As insinuated in 3 5 and 3 6 nat int and inductive datatypes are normally monotonic and treated as such The same is true for record types rat and real Thus given the cardinality specification 1 10 a formula involving nat int int list rat and rat list will lead Nitpick to consider only 10 scopes instead of 10 10000 On the other hand typedefs and quotient types are generally nonmonotonic 3 12 Inductive Properties Inductive properties are a particular pain to prove because the failure to establish an induction step can mean several things 1 The property is invalid 2 The property is valid but is too weak to support the induction step 3 The property is valid and strong enough it s just that we haven t found the proof yet Depending on which scenario applies we would take the appropriate course of action 1 Repair the statement of the property so that it becomes valid 2 Generalize the property and or prove auxiliary properties 3 Work harder on a proof 25 How can we distinguish between the three scenarios Nitpick s normal mode of operation can often detect scenario 1 and Isabelle s automatic tactics help with scenario 3 Using appropriate techniques it is also often possible to use Nitpick to identify scenario 2 Consider the following transition system i
39. g 33 string list A space separated list of strings e g ichi ni san bool true or false smart bool true false or smart smart_ int An integer or smart int range An integer e g 3 or a range of nonnegative integers int An integer Negative integers are prefixed with a hyphen e g 1 4 The range symbol lt emdash gt can be entered as hyphen or nt seq A comma separated sequence of ranges of integers e g 1 3 6 8 float An floating point number e g 0 5 or 60 expressing a number of seconds const The name of a HOL constant term A HOL term e g f x term list A space separated list of HOL terms e g f g y e type A HOL type Default values are indicated in curly brackets Boolean options have a negated counterpart e g blocking vs non blocking When setting them true may be omitted 5 1 Mode of Operation blocking bool true neg non_ blocking Specifies whether the nitpick command should operate synchronously The asynchronous non blocking mode lets the user start proving the putative theorem while Nitpick looks for a counterexample but it can also be more confusing For technical reasons automatic runs currently always block falsify bool true neg satisfy Specifies whether Nitpick should look for falsifying examples coun termodels or satisfying examples mod
40. g The same assumption occurs twice and the variable w is unconstrained Clearly one of the two occurrences of v in the assumptions should have been a w With the correction made we don t get any counterexample from Nitpick Let s move on and check completeness theorem S_ complete length x w x al length x w x 6 w S nitpick Nitpick found a counterexample Free variable w b b a a Apparently b b a a S even though it has the same numbers of a s and b s But since our inductive definition passed the soundness check the introduction rules we have are probably correct Perhaps we simply lack an introduction rule Comparing the grammar with the inductive definition our suspicion is confirmed Joe Blow simply forgot the production A 5AA without which the grammar cannot generate two or more b s in a row So we add the rule v A w e A b vQweE A With this last change we don t get any counterexamples from Nitpick for either soundness or completeness We can even generalize our result to cover A and B as well theorem S A B sound and complete w S 4 length x w x al length w x op w A 3 length x w x a length x w z b 1 w B 4 length x 4 w x b length x w x 1 nitpick i E Nitpick found no counterexample 4 2 AA Trees AA trees are a kind of balanced trees disco
41. he nitpick xxx attributes and the Nitpick_ xxx register yyy functions can cause havoc if used improperly e Although this has never been observed arbitrary theorem morphisms could possibly confuse Nitpick resulting in spurious counterexamples e All constants types free variables and schematic variables whose names start with Nitpick are reserved for internal use References 1 A Andersson Balanced search trees made simple In F K H A Dehne N Santoro and S Whitesides editors WADS 1993 volume 709 of Lec ture Notes in Computer Science pages 61 70 Springer Verlag 1993 53 2 3 4 5 6 7 8 9 S Berghofer and T Nipkow Random testing in Isabelle HOL In J Cuel lar and Z Liu editors SEFM 2004 pages 230 239 IEEE Computer Society Press 2004 J C Blanchette and T Nipkow Nitpick A counterexample generator for higher order logic based on a relational model finder In M Kaufmann and L Paulson editors Interactive Theorem Proving ITP 10 Lecture Notes in Computer Science Springer Verlag 2010 D Jackson Software Abstractions Logic Language and Analysis MIT Press 2006 T Nipkow L C Paulson and M Wenzel Isabelle HOL A Proof Assis tant for Higher Order Logic volume 2283 of Lecture Notes in Computer Science Springer Verlag 2002 E Torlak Kodkod Constraint solver for relational logic http alloy mit edu kodkod E Torlak and D Jackson Kodko
42. here is usu ally no need to systematically enumerate cardinalities If Nitpick cannot find a genuine counterexample for card a list 10 it is very unlikely that one could be found for smaller cardinalities 3 7 Typedefs Quotient Types Records Rationals and Reals Nitpick generally treats types declared using typedef as datatypes whose single constructor is the corresponding Abs function For example typedef three 0 nat 1 2 by blast definition A three where A Abs three 0 definition B three where B Abs three 1 definition C three where C Abs three 2 lemma JA X B X ce X 12 nitpick show types Nitpick found a counterexample Free variables X 0 l c 2 Types nat 0 1 2 three 0 1 K2 In the output above n abbreviates Abs three n Quotient types are handled in much the same way The following fragment defines the integer type my_ int by encoding the integer x by a pair of natural numbers m n such that z n m fun my int rel where my int_rel x y u v 2 z v uc y quotient type my int nat x nat my int rel by auto simp add equivp def fun eq iff definition add raw where add raw A z y u v x uznat y v nat quotient definition add my int gt my_int gt my int is add raw lemma add x y add x x nitpick show types Nitpick found a counterexample
43. inductive datatype but allows infinite objects Thus the infinite lists ps a a a qs a b a b and rs 0 1 2 3 can be defined as coinductive lists or lazy lists using the LNil a llist and LCons a a llist a llist constructors Although it is otherwise no friend of infinity Nitpick can find counter examples involving cyclic lists such as ps and qs above as well as finite lists codatatype a llist LNil LCons a a llis lemma zs Z LCons a xs nitpick Nitpick found a counterexample for card a 1 Free variables a 01 zs THE w w LCons a w The notation THE w w t w stands for the infinite term t t t Hence zs is simply the infinite list a1 a1 a1 The next example is more interesting primcorec iterates where iterates f a LCons a iterates f f a lemma vs LCons a zs ys iterates Ab a b gt xs ys nitpick verbose The type a passed the monotonicity test Nitpick might be able to skip some scopes Trying 10 scopes card a 1 card a list 1 and bisim_ depth 0 card a 10 card a list 10 and bisim_ depth 9 19 Nitpick found a counterexample for card a 2 card a llist 2 and bisim_ depth 1 Free variables a di b a2 zs THE w w LCons a w ys LCons a THE w w LCons a w Total time 1 11 s The lazy list zs is simply a a1 whereas ys is a5 a a1
44. itpick Isar structure val default params theory string x string list gt params The second argument lets you override option values before they are parsed and put into a params record Here is an example where Nitpick is invoked on subgoal i of n with no time limit val params Nitpick_Isar default_ params thy timeout none val outcome state Nitpick pick mits in subgoal state params Nitpick Normal i n 7 2 Registering Term Postprocessors It is possible to change the output of any term that Nitpick considers a datatype by registering a term postprocessor The interface for registering and unregistering postprocessors consists of the following pair of functions defined in the Nitpick Model structure type term_ postprocessor Proof context string typ gt term list typ gt term term val register term postprocessor typ term_ postprocessor morphism Context generic Context generic val unregister_term_ postprocessor typ morphism Context generic Context generic 83 7 and src HOL Library Multiset thy illustrate this feature in context 7 3 Registering Coinductive Datatypes Coinductive datatypes defined using the codatatype command that do not involve nested recursion through non codatatypes are supported by Nitpick If you have defined a custom coinductive datatype you can tell Nitpick about it so that it can use an efficient Kodkod axiomatization The interface for
45. lemma r A gt THE y y A A nitpick show consts Nitpick found a counterexample for card a 3 Free variables A a2 a3 T 03 Constant THEy y A 2a As the result of an optimization Nitpick directly assigned a value to the subterm THE y y A rather than to the The constant We can disable this optimization by using the command nitpick dont_ specialize show consts Our misadventures with THE suggest adding 3 z there exists a unique z such that at the front of our putative lemma s assumption lemma Jlr z A THE y y E A A The fix appears to work nitpick Nitpick found no counterexample We can further increase our confidence in the formula by exhausting all car dinalities up to 50 nitpick card a 1 50 Nitpick found no counterexample Let s see if Sledgehammer can find a proof sledgehammer Sledgehammer e on goal Try this by metis theI 42 ms by metis thel This must be our lucky day 3 4 Skolemization Are all invertible functions onto Let s find out lemma Jg Yz g f 2 So gt Vy x y f r nitpick Nitpick found a counterexample for card a 2 and card b 1 Free variable f Ax b a Skolem constants g Az J a bi 5 bi Y a The Isabelle HOL notation f x y denotes the function that maps z to y and that otherwise behaves like f Although f is the o
46. mental SAT solver such as MiniSat_JNI recommended and SAT4J Be aware that many of the counterexamples may be identical See also check potential 85 4 and sat_ solver 85 6 maz genuine int 1 Specifies the maximum number of genuine counterexamples to display If you set this option to a value greater than 1 you will need an incre mental SAT solver such as MiniSat JNI recommended and SAT4J Be aware that many of the counterexamples may be identical See also check genuine 85 4 and sat_ solver 85 6 eval term list Specifies the list of terms whose values should be displayed along with counterexamples This option suffers from an observer effect Nitpick might find different counterexamples for different values of this option atoms type string list Specifies the names to use to refer to the atoms of the given type By default Nitpick generates names of the form q where a is the first letter of the type s name atoms string list Specifies the default names to use to refer to atoms of any type For example to call the three atoms of type a ichi ni and san instead of a a2 a3 specify the option atoms a ichi ni san The default names can be overridden on a per type basis using the atoms type option described above format term int_ seq Specifies how to uncurry the value displayed for a variable or constant Uncurrying sometimes increases the readability of th
47. n which natural numbers represent states inductive set reach where 4 nat reach In lt 4 n reach gt 3 n 4 1 reach n reach gt n 2 reach We will try to prove that only even numbers are reachable lemma n reach 2 dvd n Does this property hold Nitpick cannot find a counterexample within 30 seconds so let s attempt a proof by induction apply induct set reach apply auto This leaves us in the following proof state goal 2 subgoals 1 An n reach n lt 4 2 dvd n gt 2 dvd Suc 3 n 2 An n reach 2 dvd n gt 2 dvd Suc Suc n If we run Nitpick on the first subgoal it still won t find any counterexample and yet auto fails to go further and arith is helpless However notice the n reach assumption which strengthens the induction hypothesis but is not immediately usable in the proof If we remove it and invoke Nitpick this time we get a counterexample apply thin tac n reach nitpick Nitpick found a counterexample Skolem constant n 0 Indeed 0 lt 4 2 divides 0 but 2 does not divide 1 We can use this infor mation to strength the lemma lemma n reach gt 2 dvd n V n 40 26 Unfortunately the proof by induction still gets stuck except that Nitpick now finds the counterexample n 2 We generalize the lemma further to lemma n reach gt 2 dvd nV n gt 4 and this time arith can
48. n can be used incre mentally Riss3g Riss3g is an efficient solver written in C To use Riss3g set the environment variable RISS3G_HOME to the direc tory that contains the riss3g executable The C sources for Riss3g are available at http tools computational logic org content riss3g php Nitpick has been tested with the SAT Competition 2013 version zChaff zChaff is an older solver written in C To use zChaff set the environment variable ZCHAFF_HOME to the direc tory that contains the zchaff executable The C sources and executables for zChaff are available at http www princeton edu chaff zchaff html Nitpick has been tested with versions 2004 05 13 2004 11 15 and 2007 03 12 RSat RSat is an efficient solver written in C To use RSat set the environment variable RSAT_HOME to the directory that contains the rsat executable The C sources for RSat are available at http reasoning cs ucla edu rsat Nitpick has been tested with version 2 01 BerkMin BerkMin561 is an efficient solver written in C To use BerkMin set the environment variable BERKMIN HOME to the direc tory that contains the BerkMin561 executable The BerkMin ex ecutables are available at http eigold tripod com BerkMin html BerkMin Alloy Variant of BerkMin that is included with Al loy 4 and calls itself sat56 in its banner text To use this version of BerkMin set the environment variable BERKMINALLOY HOME to the directory that
49. nce 47 7 Standard ML Interface 50 7 1 Invoking Nitpick 2 ume aaa Ree a Ree e i wee 50 7 2 Registering Term Post processors 2 4 ae Bee ee 51 7 3 Registering Coinductive Datatypes 51 8 Known Bugs and Limitations 52 1 Introduction Nitpick 3 is a counterexample generator for Isabelle HOL 5 that is de signed to handle formulas combining co inductive datatypes co inductively defined predicates and quantifiers It builds on Kodkod 7 a highly opti mized first order relational model finder developed by the Software Design Group at MIT It is conceptually similar to Refute 8 from which it borrows many ideas and code fragments but it benefits from Kodkod s optimizations and a new encoding scheme The name Nitpick is shamelessly appropriated from a now retired Alloy precursor Nitpick is easy to use you simply enter nitpick after a putative theorem and wait a few seconds Nonetheless there are situations where knowing how it works under the hood and how it reacts to various options helps increase the test coverage This manual also explains how to install the tool on your workstation Should the motivation fail you think of the many hours of hard work Nitpick will save you Proving non theorems is hard work Another common use of Nitpick is to find out whether the axioms of a locale are satisfiable while the locale is being developed To check this it suffices to write lemma False nitpick show all
50. nly free variable The symbol can be entered as hyphen or lt emdash gt occurring in the formula Nitpick also displays values for the bound vari ables g and y These values are available to Nitpick because it performs skolemization as a preprocessing step In the previous example skolemization only affected the outermost quanti fiers This is not always the case as illustrated below lemma dz Vf f z nitpick Nitpick found a counterexample for card a 2 Skolem constant Ax f Ax _ a Az GG a az Az a4 a a5 a The variable f is bound within the scope of x therefore f depends on z as suggested by the notation Az f If x a then f is the function that maps a to and vice versa otherwise r a and f maps both a and a to ay In both cases f x z x The source of the Skolem constants is sometimes more obscure lemma refl r gt sym r nitpick Nitpick found a counterexample for card a 2 Free variable r a1 a az a1 a2 az Skolem constants sym rz a sym y a What happened here is that Nitpick expanded sym to its definition sym r Yz y x y E r y x Er As their names suggest the Skolem constants sym r and sym y are simply the bound variables z and y from sym s definition 3 5 Natural Numbers and Integers Because of the axiom of infinity the type nat does not admit any finite models To deal with this
51. on in conjunction with the introduction rules To override this you can specify an alternative definition as follows lemma odd alt unfold nitpick unfold odd n n mod 2 1 Nitpick then expands all occurrences of odd n to n mod 2 1 Alternatively you can specify an equational specification of the constant lemma odd simp nitpick_simp odd n n mod 2 1 Such tweaks should be done with great care because Nitpick will assume that the constant is completely defined by its equational specification For example if you make odd 2 x k 1 a nitpick simp rule and neglect to provide rules to handle the 2 k case Nitpick will define odd n arbitrarily for even values of n The debug 85 3 option is extremely useful to understand what is going on when experimenting with nitpick_ attributes Because of its internal three valued logic Nitpick tends to lose a lot of pre cision in the presence of partially specified constants For example lemma odd simp nitpick_ simp odd x even x is superior to 49 lemma odd_psimps nitpick_ simp even xz gt odd x False even odd x True Because Nitpick sometimes unfolds definitions but never simplification rules you can ensure that a constant is defined explicitly using the nztpick_ simp For example definition optimum where nitpick simp optimum t Vu consistent u alphabet t alphabet u freq t freq u cost t lt
52. option is implicitly disabled for automatic runs See also spy 85 1 overlord 85 1 and batch size 85 6 show types E bool false neg hide_ types Specifies whether the subsets used to approximate co inductive data types should be displayed as part of counterexamples Such subsets are sometimes helpful when investigating whether a potentially spurious counterexample is genuine but their potential for clutter is real show skolems bool true neg hide skolem Specifies whether the values of Skolem constants should be displayed as part of counterexamples Skolem constants correspond to bound variables in the original formula and usually help us to understand why the counterexample falsifies the formula show consts bool false neg hide consts Specifies whether the values of constants occurring in the formula in cluding its axioms should be displayed along with any counterexample These values are sometimes helpful when investigating why a counter example is genuine but they can clutter the output show all bool Abbreviation for show types show skolems and show consts maz potential int 1 Specifies the maximum number of potentially spurious counterexamples to display Setting this option to 0 speeds up the search for a genuine counterexample This option is implicitly set to 0 for automatic runs 40 If you set this option to a value greater than 1 you will need an incre
53. packages Nitpick relies on the more natural equational specification entered by the user Behind the scenes Isabelle s built in packages and theories rely on the fol lowing attributes to affect Nitpick s behavior nitpick unfold This attribute specifies an equation that Nitpick should use to expand a constant The equation should be logically equivalent to the constant s actual definition and should be of the form e Tp ui Tg t Or II SUR C m liy 47 where 21 are distinct variables and c does not occur in t Each occurrence of c in the problem is expanded to Az Xp t nitpick simp This attribute specifies the equations that constitute the specification of a constant The primrec function and nominal primrec pack ages automatically attach this attribute to their s mps rules The equa tions must be of the form C iu u Or ch th u nitpick psimp This attribute specifies the equations that constitute the partial spec ification of a constant The function package automatically attaches this attribute to its psimps rules The conditional equations must be of the form Or Pass Pa c h use tn E C nitpick choice spec This attribute specifies the free form specification of a constant de fined using the ax specification command When faced with a constant Nitpick proceeds as follows il If the nitpick simp set associated with the constant is not empty Nit pick uses th
54. r theory file should start as follows theory Scratch imports Main Quotient Product RealDef begin The results presented here were obtained using the JNI Java Native Inter face version of MiniSat and with multithreading disabled to reduce nonde terminism This was done by adding the line nitpick params sat solver MiniSat JNI max threads 1 after the begin keyword The JNI version of MiniSat is bundled with Kod kodi and is precompiled for Linux Mac OS X and Windows Cygwin Other SAT solvers can also be used as explained in 85 6 If you have already con figured SAT solvers in Isabelle e g for Refute these will also be available to Nitpick 3 1 Propositional Logic Let s start with a trivial example from propositional logic lemma P lt gt Q nitpick You should get the following output Nitpick found a counterexample Free variables P True Q False Nitpick can also be invoked on individual subgoals as in the example below apply auto goal 2 subgoals 1 P Q 2 Q gt P nitpick 1 Nitpick found a counterexample Free variables P True Q False nitpick 2 Nitpick found a counterexample Free variables P False Q True oops 3 2 Type Variables If you are left unimpressed by the previous example don t worry The next one is more mind and computer boggling lemma r A gt THE y y A A The putative lemma involves the definite desc
55. reads to use in Kodkod If this option is set to 0 Kodkod will compute an appropriate value based on the number of processor cores available The option is implicitly set to 1 for automatic runs See also batch size 85 6 and timeout 85 7 46 5 7 Timeouts timeout float 30 Specifies the maximum number of seconds that the nitpick command should spend looking for a counterexample Nitpick tries to honor this constraint as well as it can but offers no guarantees For automatic runs the Auto Time Limit option under Plugins gt Plugin Options gt Isabelle gt General is used instead See also max threads 85 6 tac timeout float 10 5 Specifies the maximum number of seconds that should be used by internal tactics lexicographic order and size change when checking whether a co inductive predicate is well founded auto tactic when checking a counterexample or the monotonicity inference Nitpick tries to honor this constraint but offers no guarantees See also wf 85 2 mono 85 2 check potential 85 4 and check genuine 85 4 6 Attribute Reference Nitpick needs to consider the definitions of all constants occurring in a for mula in order to falsify it For constants introduced using the definition command the definition is simply the associated _ def axiom In contrast instead of using the internal representation of functions synthesized by Isa belle s primrec function and nominal primrec
56. ription operator THE pre sented in section 5 10 1 of the Isabelle tutorial 5 The operator is defined by the axiom THE z a a The putative lemma is merely asserting the indefinite description operator axiom with THE substituted for SOME The free variable x and the bound variable y have type a For formulas containing type variables Nitpick enumerates the possible domains for each type variable up to a given cardinality 10 by default looking for a finite countermodel nitpick verbose Trying 10 scopes card a 1 card a 2 card a 10 Nitpick found a counterexample for card a 3 Free variables A da az T 03 Total time 963 ms Nitpick found a counterexample in which a has cardinality 3 For cardinal ities 1 and 2 the formula holds In the counterexample the three values of type a are written a1 a and aa The message Trying n scopes is shown only if the option verbose is enabled You can specify verbose each time you invoke nitpick or you can set it globally using the command nitpick_ params verbose This command also displays the current default values for all of the options supported by Nitpick The options are listed in 5 3 3 Constants By just looking at Nitpick s output it might not be clear why the counter example in 3 2 is genuine Let s invoke Nitpick again this time telling it to show the values of the constants that occur in the formula
57. roofs Developing theo ries this way usually saves time because faulty theorems and definitions are discovered much earlier in the process 5 Option Reference Nitpick s behavior can be influenced by various options which can be speci fied in brackets after the nitpick command Default values can be set using nitpick params For example nitpick params verbose timeout 60 The options are categorized as follows mode of operation 5 1 scope of search 85 2 output format 85 3 automatic counterexample checks 85 4 regression testing 85 5 optimizations 85 6 and timeouts 85 7 If you use Isabelle jEdit Nitpick also provides an automatic mode that can be enabled via the Auto Nitpick option under Plugins gt Plugin Options gt Isabelle gt General For automatic runs user azioms 85 1 assms 85 1 and mono 85 2 are implicitly enabled blocking 85 1 verbose 85 3 and debug 85 3 are disabled max threads 85 6 is taken to be 1 maz_ potential 85 3 is taken to be 0 and timeout 85 7 is superseded by the Auto Time Limit in jEdit Nitpick s output is also more concise The number of options can be overwhelming at first glance Do not let that worry you Nitpick s defaults have been chosen so that it almost always does the right thing and the most important options have been covered in context in 83 The descriptions below refer to the following syntactic quantities e string A strin
58. s LCons a ys gt zs ys nitpick bisim depth 1 show types Nitpick found a quasi genuine counterexample for card a 2 20 Free variables a a vs THE w w LCons a w ys THE w w LCons a w Type a llist THE w w LCons ay w THE w w LCons ai w Try again with bisim depth set to a nonnegative value to confirm that the counterexample is genuine nitpick Nitpick found no counterexample In the first nitpick invocation the after the fact check discovered that the two known elements of type a llist are bisimilar prompting Nitpick to label the example as only quasi genuine A compromise between leaving out the bisimilarity predicate from the Kod kod problem and performing the after the fact check is to specify a low non negative bisim_ depth value In general a value of K means that Nitpick will require all lists to be distinguished from each other by their prefixes of length K However setting K to a too low value can overconstrain Nitpick preventing it from finding any counterexamples 3 10 Boxing Nitpick normally maps function and product types directly to the corre sponding Kodkod concepts As a consequence if a has cardinality 3 and b has cardinality 4 then a x b has cardinality 12 4 x 3 and a b has cardinality 64 4 In some circumstances it pays off to treat these types in the same way as plain datatypes by approximating them by a subset of a given
59. the max const option described above binary ints smart_bool smart neg unary _ ints Specifies whether natural numbers and integers should be encoded us ing a unary or binary notation In unary mode the cardinality fully specifies the subset used to approximate the type For example card nat 4 induces 0 1 2 3 card int 4 induces 1 0 1 2 card int 5 induces 2 1 0 1 2 In general card nat K induces 0 K 1 card ini K induces K 2 1 K 2 In binary mode the cardinality specifies the number of distinct values that can be constructed Each of these value is represented by a bit pattern whose length is specified by the bits 85 2 option By default 36 Nitpick attempts to choose the more appropriate encoding by inspect ing the formula at hand preferring the binary notation for problems involving multiplicative operators or large constants Warning For technical reasons Nitpick always reverts to unary for problems that refer to the types rat or real or the constants Suc gcd or lem See also bits 85 2 and show types 85 3 bits int seq 1 10 Specifies the number of bits to use to represent natural numbers and integers in binary excluding the sign bit The minimum is 1 and the maximum is 31 See also binary ints 85 2 wf const smart bool neg non wf Specifies whether the specified co inductively defined predicate is well
60. ven scopes or lies outside Nitpick s supported fragment Only potentially spurious If an inductive predicate is well founded then it has exactly one fixed point which is simultaneously the least and the greatest fixed point In these circumstances the com putation of the least fixed point amounts to the computation of an arbitrary fixed point which can be performed using a straightforward recursive equation 15 counterexamples may be found Nitpick found a potentially spurious counterexample for card nat 50 Empty assignment Nitpick could not find a better counterexample It checked 1 of 1 scope Total time 1 62 s No genuine counterexample is possible because Nitpick cannot rule out the existence of a natural number n gt 50 such that both even n and even Suc n are true To help Nitpick we can bound the existential quantifier lemma Jn lt 49 even n even Suc n nitpick card nat 50 unary_ ints Nitpick found a counterexample Empty assignment 5o far we were blessed by the wellfoundedness of even What happens if we use the following definition instead inductive even where even 0 nat even 2 Jeven m even n even m n This definition is not well founded From even 0 and even 0 we can derive that even 0 Nonetheless the predicates even and even are equivalent Let s check a property involving even To make up for the foreseeable com putational hur
61. vered by Arne Andersson that provide similar performance to red black trees but with a simpler imple mentation 1 They can be used to store sets of elements equipped with a 29 total order lt We start by defining the datatype and some basic extractor functions datatype a aa tree f A N azlinorder nat a aa tree a aa tree primrec data where data A Ax _ data tN a lpeNE primrec dataset where dataset A dataset N x _ t u x U dataset t U dataset u primrec level where level A 0 level N _ _k__ k primrec left where left A A left N Z t_ s primrec right where right A A rigt NM _ c uw The wellformedness criterion for AA trees is fairly complex Wikipedia states it as follows 9 Each node has a level field and the following invariants must remain true for the tree to be valid 1 The level of a leaf node is one 2 The level of a left child is strictly less than that of its parent 3 The level of a right child is less than or equal to that of its parent 4 The level of a right grandchild is strictly less than that of its grandparent 5 Every node of level greater than one must have two children The wf predicate formalizes this description primrec wf where wf A True 30 faf N ktu if t A then k 1 u A V levelu 1 left u A right u A else wf t wfu wuZzNM lev

Download Pdf Manuals

Related Search

Related Contents

液面計用部品カタログ 2014年12月1日（更新） 1.09MB  Suanovil 20 sol. inj.  Sillage n°122    Guía para la revisión de Enlaces Inalámbricos  Libretto Istruzioni Thermo  Panas。nic  Samsung PS-42C62H Bruksanvisning  

Copyright © All rights reserved. Failed to retrieve file