465 \prew |
465 \prew |
466 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] |
466 \textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$] |
467 \postw |
467 \postw |
468 |
468 |
469 With infinite types, we don't always have the luxury of a genuine counterexample |
469 With infinite types, we don't always have the luxury of a genuine counterexample |
470 and must often content ourselves with a potential one. The tedious task of |
470 and must often content ourselves with a potentially spurious one. The tedious |
471 finding out whether the potential counterexample is in fact genuine can be |
471 task of finding out whether the potentially spurious counterexample is in fact |
472 outsourced to \textit{auto} by passing \textit{check\_potential}. For example: |
472 genuine can be delegated to \textit{auto} by passing \textit{check\_potential}. |
|
473 For example: |
473 |
474 |
474 \prew |
475 \prew |
475 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ |
476 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ |
476 \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount] |
477 \textbf{nitpick} [\textit{card~nat}~= 50, \textit{check\_potential}] \\[2\smallskipamount] |
477 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported |
478 \slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported |
478 fragment. Only potential counterexamples may be found. \\[2\smallskipamount] |
479 fragment. Only potentially spurious counterexamples may be found. \\[2\smallskipamount] |
479 Nitpick found a potential counterexample: \\[2\smallskipamount] |
480 Nitpick found a potentially spurious counterexample: \\[2\smallskipamount] |
480 \hbox{}\qquad Free variable: \nopagebreak \\ |
481 \hbox{}\qquad Free variable: \nopagebreak \\ |
481 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] |
482 \hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount] |
482 Confirmation by ``\textit{auto}'': The above counterexample is genuine. |
483 Confirmation by ``\textit{auto}'': The above counterexample is genuine. |
483 \postw |
484 \postw |
484 |
485 |
485 You might wonder why the counterexample is first reported as potential. The root |
486 You might wonder why the counterexample is first reported as potentially |
486 of the problem is that the bound variable in $\forall n.\; \textit{Suc}~n |
487 spurious. The root of the problem is that the bound variable in $\forall n.\; |
487 \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds an $n$ such |
488 \textit{Suc}~n \mathbin{\not=} n$ ranges over an infinite type. If Nitpick finds |
488 that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to |
489 an $n$ such that $\textit{Suc}~n \mathbin{=} n$, it evaluates the assumption to |
489 \textit{False}; but otherwise, it does not know anything about values of $n \ge |
490 \textit{False}; but otherwise, it does not know anything about values of $n \ge |
490 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not |
491 \textit{card~nat}$ and must therefore evaluate the assumption to $\unk$, not |
491 \textit{True}. Since the assumption can never be satisfied, the putative lemma |
492 \textit{True}. Since the assumption can never be satisfied, the putative lemma |
492 can never be falsified. |
493 can never be falsified. |
493 |
494 |
795 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] |
796 \textbf{nitpick}~[\textit{card nat}~= 50, \textit{unary\_ints}, \textit{verbose}] \\[2\smallskipamount] |
796 \slshape The inductive predicate ``\textit{even}'' was proved well-founded. |
797 \slshape The inductive predicate ``\textit{even}'' was proved well-founded. |
797 Nitpick can compute it efficiently. \\[2\smallskipamount] |
798 Nitpick can compute it efficiently. \\[2\smallskipamount] |
798 Trying 1 scope: \\ |
799 Trying 1 scope: \\ |
799 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] |
800 \hbox{}\qquad \textit{card nat}~= 50. \\[2\smallskipamount] |
800 Nitpick found a potential counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] |
801 Nitpick found a potentially spurious counterexample for \textit{card nat}~= 50: \\[2\smallskipamount] |
801 \hbox{}\qquad Empty assignment \\[2\smallskipamount] |
802 \hbox{}\qquad Empty assignment \\[2\smallskipamount] |
802 Nitpick could not find a better counterexample. It checked 0 of 1 scope. \\[2\smallskipamount] |
803 Nitpick could not find a better counterexample. \\[2\smallskipamount] |
803 Total time: 1.43 s. |
804 Total time: 1.43 s. |
804 \postw |
805 \postw |
805 |
806 |
806 No genuine counterexample is possible because Nitpick cannot rule out the |
807 No genuine counterexample is possible because Nitpick cannot rule out the |
807 existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and |
808 existence of a natural number $n \ge 50$ such that both $\textit{even}~n$ and |
2187 \textit{batch\_size} (\S\ref{optimizations}).} |
2188 \textit{batch\_size} (\S\ref{optimizations}).} |
2188 |
2189 |
2189 \opfalse{show\_datatypes}{hide\_datatypes} |
2190 \opfalse{show\_datatypes}{hide\_datatypes} |
2190 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should |
2191 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should |
2191 be displayed as part of counterexamples. Such subsets are sometimes helpful when |
2192 be displayed as part of counterexamples. Such subsets are sometimes helpful when |
2192 investigating whether a potential counterexample is genuine or spurious, but |
2193 investigating whether a potentially spurious counterexample is genuine, but |
2193 their potential for clutter is real. |
2194 their potential for clutter is real. |
2194 |
2195 |
2195 \opfalse{show\_consts}{hide\_consts} |
2196 \opfalse{show\_consts}{hide\_consts} |
2196 Specifies whether the values of constants occurring in the formula (including |
2197 Specifies whether the values of constants occurring in the formula (including |
2197 its axioms) should be displayed along with any counterexample. These values are |
2198 its axioms) should be displayed along with any counterexample. These values are |
2200 |
2201 |
2201 \opnodefault{show\_all}{bool} |
2202 \opnodefault{show\_all}{bool} |
2202 Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}. |
2203 Abbreviation for \textit{show\_datatypes} and \textit{show\_consts}. |
2203 |
2204 |
2204 \opdefault{max\_potential}{int}{\upshape 1} |
2205 \opdefault{max\_potential}{int}{\upshape 1} |
2205 Specifies the maximum number of potential counterexamples to display. Setting |
2206 Specifies the maximum number of potentially spurious counterexamples to display. |
2206 this option to 0 speeds up the search for a genuine counterexample. This option |
2207 Setting this option to 0 speeds up the search for a genuine counterexample. This |
2207 is implicitly set to 0 for automatic runs. If you set this option to a value |
2208 option is implicitly set to 0 for automatic runs. If you set this option to a |
2208 greater than 1, you will need an incremental SAT solver, such as |
2209 value greater than 1, you will need an incremental SAT solver, such as |
2209 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of |
2210 \textit{MiniSat\_JNI} (recommended) and \textit{SAT4J}. Be aware that many of |
2210 the counterexamples may be identical. |
2211 the counterexamples may be identical. |
2211 |
2212 |
2212 \nopagebreak |
2213 \nopagebreak |
2213 {\small See also \textit{check\_potential} (\S\ref{authentication}) and |
2214 {\small See also \textit{check\_potential} (\S\ref{authentication}) and |
2267 \subsection{Authentication} |
2268 \subsection{Authentication} |
2268 \label{authentication} |
2269 \label{authentication} |
2269 |
2270 |
2270 \begin{enum} |
2271 \begin{enum} |
2271 \opfalse{check\_potential}{trust\_potential} |
2272 \opfalse{check\_potential}{trust\_potential} |
2272 Specifies whether potential counterexamples should be given to Isabelle's |
2273 Specifies whether potentially spurious counterexamples should be given to |
2273 \textit{auto} tactic to assess their validity. If a potential counterexample is |
2274 Isabelle's \textit{auto} tactic to assess their validity. If a potentially |
2274 shown to be genuine, Nitpick displays a message to this effect and terminates. |
2275 spurious counterexample is shown to be genuine, Nitpick displays a message to |
|
2276 this effect and terminates. |
2275 |
2277 |
2276 \nopagebreak |
2278 \nopagebreak |
2277 {\small See also \textit{max\_potential} (\S\ref{output-format}).} |
2279 {\small See also \textit{max\_potential} (\S\ref{output-format}).} |
2278 |
2280 |
2279 \opfalse{check\_genuine}{trust\_genuine} |
2281 \opfalse{check\_genuine}{trust\_genuine} |
2292 \begin{enum} |
2294 \begin{enum} |
2293 \item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample. |
2295 \item[$\bullet$] \textbf{\textit{genuine}:} Nitpick found a genuine counterexample. |
2294 \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi |
2296 \item[$\bullet$] \textbf{\textit{quasi\_genuine}:} Nitpick found a ``quasi |
2295 genuine'' counterexample (i.e., a counterexample that is genuine unless |
2297 genuine'' counterexample (i.e., a counterexample that is genuine unless |
2296 it contradicts a missing axiom or a dangerous option was used inappropriately). |
2298 it contradicts a missing axiom or a dangerous option was used inappropriately). |
2297 \item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potential counterexample. |
2299 \item[$\bullet$] \textbf{\textit{potential}:} Nitpick found a potentially |
|
2300 spurious counterexample. |
2298 \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample. |
2301 \item[$\bullet$] \textbf{\textit{none}:} Nitpick found no counterexample. |
2299 \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g., |
2302 \item[$\bullet$] \textbf{\textit{unknown}:} Nitpick encountered some problem (e.g., |
2300 Kodkod ran out of memory). |
2303 Kodkod ran out of memory). |
2301 \end{enum} |
2304 \end{enum} |
2302 |
2305 |