doc-src/Nitpick/nitpick.tex
 changeset 41992 0e4716fa330a parent 41985 09b75d55008f child 41993 bd6296de1432
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Thu Mar 17 14:43:51 2011 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex	Thu Mar 17 14:43:53 2011 +0100
1.3 @@ -467,25 +467,26 @@
1.4  \postw
1.5
1.6  With infinite types, we don't always have the luxury of a genuine counterexample
1.7 -and must often content ourselves with a potential one. The tedious task of
1.8 -finding out whether the potential counterexample is in fact genuine can be
1.9 -outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
1.10 +and must often content ourselves with a potentially spurious one. The tedious
1.11 +task of finding out whether the potentially spurious counterexample is in fact
1.12 +genuine can be delegated to \textit{auto} by passing \textit{check\_potential}.
1.13 +For example:
1.14
1.15  \prew
1.16  \textbf{lemma} $\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.17  \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount]
1.18  \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
1.19 -fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
1.20 -Nitpick found a potential counterexample: \\[2\smallskipamount]
1.21 +fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount]
1.22 +Nitpick found a potentially spurious counterexample: \\[2\smallskipamount]
1.23  \hbox{}\qquad Free variable: \nopagebreak \\
1.24  \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
1.25  Confirmation by \textit{auto}'': The above counterexample is genuine.
1.26  \postw
1.27
1.28 -You might wonder why the counterexample is first reported as potential. The root
1.29 -of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n 1.30 -\mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such
1.31 -that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
1.32 +You might wonder why the counterexample is first reported as potentially
1.33 +spurious. The root of the problem is that the bound variable in $\forall n.\; 1.34 +\textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds
1.35 +an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to
1.36  \textit{False}; but otherwise, it does not know anything about values of $n \ge 1.37 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not
1.38  \textit{True}. Since the assumption can never be satisfied, the putative lemma
1.39 @@ -797,9 +798,9 @@
1.40  Nitpick can compute it efficiently. \\[2\smallskipamount]
1.41  Trying 1 scope: \\
1.42  \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount]
1.43 -Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
1.44 +Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount]
1.46 -Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount]
1.47 +Nitpick could not find a better counterexample. \\[2\smallskipamount]
1.48  Total time: 1.43 s.
1.49  \postw
1.50
1.51 @@ -2189,7 +2190,7 @@
1.52  \opfalse{show\_datatypes}{hide\_datatypes}
1.53  Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
1.54  be displayed as part of counterexamples. Such subsets are sometimes helpful when
1.55 -investigating whether a potential counterexample is genuine or spurious, but
1.56 +investigating whether a potentially spurious counterexample is genuine, but
1.57  their potential for clutter is real.
1.58
1.59  \opfalse{show\_consts}{hide\_consts}
1.60 @@ -2202,10 +2203,10 @@
1.61  Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}.
1.62
1.63  \opdefault{max\_potential}{int}{\upshape 1}
1.64 -Specifies the maximum number of potential counterexamples to display. Setting
1.65 -this option to 0 speeds up the search for a genuine counterexample. This option
1.66 -is implicitly set to 0 for automatic runs. If you set this option to a value
1.67 -greater than 1, you will need an incremental SAT solver, such as
1.68 +Specifies the maximum number of potentially spurious counterexamples to display.
1.69 +Setting this option to 0 speeds up the search for a genuine counterexample. This
1.70 +option is implicitly set to 0 for automatic runs. If you set this option to a
1.71 +value greater than 1, you will need an incremental SAT solver, such as
1.72  \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of
1.73  the counterexamples may be identical.
1.74
1.75 @@ -2269,9 +2270,10 @@
1.76
1.77  \begin{enum}
1.78  \opfalse{check\_potential}{trust\_potential}
1.79 -Specifies whether potential counterexamples should be given to Isabelle's
1.80 -\textit{auto} tactic to assess their validity. If a potential counterexample is
1.81 -shown to be genuine, Nitpick displays a message to this effect and terminates.
1.82 +Specifies whether potentially spurious counterexamples should be given to
1.83 +Isabelle's \textit{auto} tactic to assess their validity. If a potentially
1.84 +spurious counterexample is shown to be genuine, Nitpick displays a message to
1.85 +this effect and terminates.
1.86
1.87  \nopagebreak
1.90  \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a quasi
1.93 -\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
1.94 +\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
1.96  \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
1.97  \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,