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.45  \hbox{}\qquad Empty assignment \\[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.88  {\small See also \textit{max\_potential} (\S\ref{output-format}).}
    1.89 @@ -2294,7 +2296,8 @@
    1.90  \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi
    1.91  genuine'' counterexample (i.e., a counterexample that is genuine unless
    1.92  it contradicts a missing axiom or a dangerous option was used inappropriately).
    1.93 -\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample.
    1.94 +\item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially
    1.95 +spurious counterexample.
    1.96  \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample.
    1.97  \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g.,
    1.98  Kodkod ran out of memory).