summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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).