1.1 --- a/doc-src/Nitpick/nitpick.tex Fri May 14 22:30:24 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri May 14 22:43:00 2010 +0200
1.3 @@ -81,7 +81,7 @@
1.4 \section{Introduction}
1.5 \label{introduction}
1.6
1.7 -Nitpick \cite{blanchette-nipkow-2009} is a counterexample generator for
1.8 +Nitpick \cite{blanchette-nipkow-2010} is a counterexample generator for
1.9 Isabelle/HOL \cite{isa-tutorial} that is designed to handle formulas
1.10 combining (co)in\-duc\-tive datatypes, (co)in\-duc\-tively defined predicates, and
1.11 quantifiers. It builds on Kodkod \cite{torlak-jackson-2007}, a highly optimized
1.12 @@ -111,6 +111,11 @@
1.13 must find a model for the axioms. If it finds no model, we have an indication
1.14 that the axioms might be unsatisfiable.
1.15
1.16 +You can also invoke Nitpick from the ``Commands'' submenu of the
1.17 +``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a
1.18 +C-n. This is equivalent to entering the \textbf{nitpick} command with no
1.19 +arguments in the theory text.
1.20 +
1.21 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual
1.22 machine called \texttt{java}. The examples presented in this manual can be found
1.23 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory.
1.24 @@ -137,6 +142,22 @@
1.25 suggesting several textual improvements.
1.26 % and Perry James for reporting a typo.
1.27
1.28 +%\section{Installation}
1.29 +%\label{installation}
1.30 +%
1.31 +%MISSING:
1.32 +%
1.33 +% * Nitpick is part of Isabelle/HOL
1.34 +% * but it relies on an external tool called Kodkodi (Kodkod wrapper)
1.35 +% * Two options:
1.36 +% * if you use a prebuilt Isabelle package, Kodkodi is automatically there
1.37 +% * if you work from sources, the latest Kodkodi can be obtained from ...
1.38 +% download it, install it in some directory of your choice (e.g.,
1.39 +% $ISABELLE_HOME/contrib/kodkodi), and add the absolute path to Kodkodi
1.40 +% in your .isabelle/etc/components file
1.41 +%
1.42 +% * If you're not sure, just try the example in the next section
1.43 +
1.44 \section{First Steps}
1.45 \label{first-steps}
1.46
1.47 @@ -184,6 +205,9 @@
1.48 \hbox{}\qquad\qquad $Q = \textit{False}$
1.49 \postw
1.50
1.51 +%FIXME: If you get the output:...
1.52 +%Then do such-and-such.
1.53 +
1.54 Nitpick can also be invoked on individual subgoals, as in the example below:
1.55
1.56 \prew
1.57 @@ -2017,17 +2041,17 @@
1.58 well-founded. The option can take the following values:
1.59
1.60 \begin{enum}
1.61 -\item[$\bullet$] \textbf{\textit{true}}: Tentatively treat the (co)in\-duc\-tive
1.62 +\item[$\bullet$] \textbf{\textit{true}:} Tentatively treat the (co)in\-duc\-tive
1.63 predicate as if it were well-founded. Since this is generally not sound when the
1.64 predicate is not well-founded, the counterexamples are tagged as ``quasi
1.65 genuine.''
1.66
1.67 -\item[$\bullet$] \textbf{\textit{false}}: Treat the (co)in\-duc\-tive predicate
1.68 +\item[$\bullet$] \textbf{\textit{false}:} Treat the (co)in\-duc\-tive predicate
1.69 as if it were not well-founded. The predicate is then unrolled as prescribed by
1.70 the \textit{star\_linear\_preds}, \textit{iter}~\qty{const}, and \textit{iter}
1.71 options.
1.72
1.73 -\item[$\bullet$] \textbf{\textit{smart}}: Try to prove that the inductive
1.74 +\item[$\bullet$] \textbf{\textit{smart}:} Try to prove that the inductive
1.75 predicate is well-founded using Isabelle's \textit{lexicographic\_order} and
1.76 \textit{size\_change} tactics. If this succeeds (or the predicate occurs with an
1.77 appropriate polarity in the formula to falsify), use an efficient fixed point
1.78 @@ -2080,10 +2104,10 @@
1.79 counterexamples. The option can take the following values:
1.80
1.81 \begin{enum}
1.82 -\item[$\bullet$] \textbf{\textit{true}}: Box the specified type whenever
1.83 +\item[$\bullet$] \textbf{\textit{true}:} Box the specified type whenever
1.84 practicable.
1.85 -\item[$\bullet$] \textbf{\textit{false}}: Never box the type.
1.86 -\item[$\bullet$] \textbf{\textit{smart}}: Box the type only in contexts where it
1.87 +\item[$\bullet$] \textbf{\textit{false}:} Never box the type.
1.88 +\item[$\bullet$] \textbf{\textit{smart}:} Box the type only in contexts where it
1.89 is likely to help. For example, $n$-tuples where $n > 2$ and arguments to
1.90 higher-order functions are good candidates for boxing.
1.91 \end{enum}
1.92 @@ -2107,8 +2131,8 @@
1.93 then take the following values:
1.94
1.95 \begin{enum}
1.96 -\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the type.
1.97 -\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}}: Finitize the
1.98 +\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
1.99 +\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
1.100 type wherever possible.
1.101 \end{enum}
1.102
1.103 @@ -2116,11 +2140,11 @@
1.104 datatypes:
1.105
1.106 \begin{enum}
1.107 -\item[$\bullet$] \textbf{\textit{true}}: Finitize the datatype. Since this is
1.108 +\item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
1.109 unsound, counterexamples generated under these conditions are tagged as ``quasi
1.110 genuine.''
1.111 -\item[$\bullet$] \textbf{\textit{false}}: Don't attempt to finitize the datatype.
1.112 -\item[$\bullet$] \textbf{\textit{smart}}: Perform a monotonicity analysis to
1.113 +\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
1.114 +\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
1.115 detect whether the datatype can be safely finitized before finitizing it.
1.116 \end{enum}
1.117
1.118 @@ -2282,13 +2306,13 @@
1.119 Specifies the expected outcome, which must be one of the following:
1.120
1.121 \begin{enum}
1.122 -\item[$\bullet$] \textbf{\textit{genuine}}: Nitpick found a genuine counterexample.
1.123 -\item[$\bullet$] \textbf{\textit{quasi\_genuine}}: Nitpick found a ``quasi
1.124 +\item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample.
1.125 +\item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
1.126 genuine'' counterexample (i.e., a counterexample that is genuine unless
1.127 it contradicts a missing axiom or a dangerous option was used inappropriately).
1.128 -\item[$\bullet$] \textbf{\textit{potential}}: Nitpick found a potential counterexample.
1.129 -\item[$\bullet$] \textbf{\textit{none}}: Nitpick found no counterexample.
1.130 -\item[$\bullet$] \textbf{\textit{unknown}}: Nitpick encountered some problem (e.g.,
1.131 +\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
1.132 +\item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
1.133 +\item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
1.134 Kodkod ran out of memory).
1.135 \end{enum}
1.136
1.137 @@ -2314,11 +2338,9 @@
1.138
1.139 The supported solvers are listed below:
1.140
1.141 -\let\foo
1.142 -
1.143 \begin{enum}
1.144
1.145 -\item[$\bullet$] \textbf{\textit{MiniSat}}: MiniSat is an efficient solver
1.146 +\item[$\bullet$] \textbf{\textit{MiniSat}:} MiniSat is an efficient solver
1.147 written in \cpp{}. To use MiniSat, set the environment variable
1.148 \texttt{MINISAT\_HOME} to the directory that contains the \texttt{minisat}
1.149 executable.%
1.150 @@ -2329,13 +2351,13 @@
1.151 \url{http://minisat.se/MiniSat.html}. Nitpick has been tested with versions 1.14
1.152 and 2.0 beta (2007-07-21).
1.153
1.154 -\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}}: The JNI (Java Native Interface)
1.155 +\item[$\bullet$] \textbf{\textit{MiniSat\_JNI}:} The JNI (Java Native Interface)
1.156 version of MiniSat is bundled with Kodkodi and is precompiled for the major
1.157 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
1.158 which you will find on Kodkod's web site \cite{kodkod-2009}. Unlike the standard
1.159 version of MiniSat, the JNI version can be used incrementally.
1.160
1.161 -\item[$\bullet$] \textbf{\textit{PicoSAT}}: PicoSAT is an efficient solver
1.162 +\item[$\bullet$] \textbf{\textit{PicoSAT}:} PicoSAT is an efficient solver
1.163 written in C. You can install a standard version of
1.164 PicoSAT and set the environment variable \texttt{PICOSAT\_HOME} to the directory
1.165 that contains the \texttt{picosat} executable.%
1.166 @@ -2344,7 +2366,7 @@
1.167 available at \url{http://fmv.jku.at/picosat/} and are also bundled with Kodkodi.
1.168 Nitpick has been tested with version 913.
1.169
1.170 -\item[$\bullet$] \textbf{\textit{zChaff}}: zChaff is an efficient solver written
1.171 +\item[$\bullet$] \textbf{\textit{zChaff}:} zChaff is an efficient solver written
1.172 in \cpp{}. To use zChaff, set the environment variable \texttt{ZCHAFF\_HOME} to
1.173 the directory that contains the \texttt{zchaff} executable.%
1.174 \footref{cygwin-paths}
1.175 @@ -2352,12 +2374,12 @@
1.176 \url{http://www.princeton.edu/~chaff/zchaff.html}. Nitpick has been tested with
1.177 versions 2004-05-13, 2004-11-15, and 2007-03-12.
1.178
1.179 -\item[$\bullet$] \textbf{\textit{zChaff\_JNI}}: The JNI version of zChaff is
1.180 +\item[$\bullet$] \textbf{\textit{zChaff\_JNI}:} The JNI version of zChaff is
1.181 bundled with Kodkodi and is precompiled for the major
1.182 platforms. It is also available from \texttt{native\-solver.\allowbreak tgz},
1.183 which you will find on Kodkod's web site \cite{kodkod-2009}.
1.184
1.185 -\item[$\bullet$] \textbf{\textit{RSat}}: RSat is an efficient solver written in
1.186 +\item[$\bullet$] \textbf{\textit{RSat}:} RSat is an efficient solver written in
1.187 \cpp{}. To use RSat, set the environment variable \texttt{RSAT\_HOME} to the
1.188 directory that contains the \texttt{rsat} executable.%
1.189 \footref{cygwin-paths}
1.190 @@ -2365,21 +2387,21 @@
1.191 \url{http://reasoning.cs.ucla.edu/rsat/}. Nitpick has been tested with version
1.192 2.01.
1.193
1.194 -\item[$\bullet$] \textbf{\textit{BerkMin}}: BerkMin561 is an efficient solver
1.195 +\item[$\bullet$] \textbf{\textit{BerkMin}:} BerkMin561 is an efficient solver
1.196 written in C. To use BerkMin, set the environment variable
1.197 \texttt{BERKMIN\_HOME} to the directory that contains the \texttt{BerkMin561}
1.198 executable.\footref{cygwin-paths}
1.199 The BerkMin executables are available at
1.200 \url{http://eigold.tripod.com/BerkMin.html}.
1.201
1.202 -\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}}: Variant of BerkMin that is
1.203 +\item[$\bullet$] \textbf{\textit{BerkMin\_Alloy}:} Variant of BerkMin that is
1.204 included with Alloy 4 and calls itself ``sat56'' in its banner text. To use this
1.205 version of BerkMin, set the environment variable
1.206 \texttt{BERKMINALLOY\_HOME} to the directory that contains the \texttt{berkmin}
1.207 executable.%
1.208 \footref{cygwin-paths}
1.209
1.210 -\item[$\bullet$] \textbf{\textit{Jerusat}}: Jerusat 1.3 is an efficient solver
1.211 +\item[$\bullet$] \textbf{\textit{Jerusat}:} Jerusat 1.3 is an efficient solver
1.212 written in C. To use Jerusat, set the environment variable
1.213 \texttt{JERUSAT\_HOME} to the directory that contains the \texttt{Jerusat1.3}
1.214 executable.%
1.215 @@ -2387,24 +2409,16 @@
1.216 The C sources for Jerusat are available at
1.217 \url{http://www.cs.tau.ac.il/~ale1/Jerusat1.3.tgz}.
1.218
1.219 -\item[$\bullet$] \textbf{\textit{SAT4J}}: SAT4J is a reasonably efficient solver
1.220 +\item[$\bullet$] \textbf{\textit{SAT4J}:} SAT4J is a reasonably efficient solver
1.221 written in Java that can be used incrementally. It is bundled with Kodkodi and
1.222 requires no further installation or configuration steps. Do not attempt to
1.223 install the official SAT4J packages, because their API is incompatible with
1.224 Kodkod.
1.225
1.226 -\item[$\bullet$] \textbf{\textit{SAT4J\_Light}}: Variant of SAT4J that is
1.227 +\item[$\bullet$] \textbf{\textit{SAT4J\_Light}:} Variant of SAT4J that is
1.228 optimized for small problems. It can also be used incrementally.
1.229
1.230 -\item[$\bullet$] \textbf{\textit{HaifaSat}}: HaifaSat 1.0 beta is an
1.231 -experimental solver written in \cpp. To use HaifaSat, set the environment
1.232 -variable \texttt{HAIFASAT\_\allowbreak HOME} to the directory that contains the
1.233 -\texttt{HaifaSat} executable.%
1.234 -\footref{cygwin-paths}
1.235 -The \cpp{} sources for HaifaSat are available at
1.236 -\url{http://cs.technion.ac.il/~gershman/HaifaSat.htm}.
1.237 -
1.238 -\item[$\bullet$] \textbf{\textit{smart}}: If \textit{sat\_solver} is set to
1.239 +\item[$\bullet$] \textbf{\textit{smart}:} If \textit{sat\_solver} is set to
1.240 \textit{smart}, Nitpick selects the first solver among MiniSat,
1.241 PicoSAT, zChaff, RSat, BerkMin, BerkMin\_Alloy, Jerusat, MiniSat\_JNI, and zChaff\_JNI
1.242 that is recognized by Isabelle. If none is found, it falls back on SAT4J, which