1.1 --- a/doc-src/Nitpick/nitpick.tex Tue Aug 03 14:49:42 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Tue Aug 03 14:54:30 2010 +0200
1.3 @@ -247,17 +247,17 @@
1.4
1.5 The free variable $x$ and the bound variable $y$ have type $'a$. For formulas
1.6 containing type variables, Nitpick enumerates the possible domains for each type
1.7 -variable, up to a given cardinality (8 by default), looking for a finite
1.8 +variable, up to a given cardinality (10 by default), looking for a finite
1.9 countermodel:
1.10
1.11 \prew
1.12 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.13 \slshape
1.14 -Trying 8 scopes: \nopagebreak \\
1.15 +Trying 10 scopes: \nopagebreak \\
1.16 \hbox{}\qquad \textit{card}~$'a$~= 1; \\
1.17 \hbox{}\qquad \textit{card}~$'a$~= 2; \\
1.18 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.19 -\hbox{}\qquad \textit{card}~$'a$~= 8. \\[2\smallskipamount]
1.20 +\hbox{}\qquad \textit{card}~$'a$~= 10. \\[2\smallskipamount]
1.21 Nitpick found a counterexample for \textit{card} $'a$~= 3: \\[2\smallskipamount]
1.22 \hbox{}\qquad Free variables: \nopagebreak \\
1.23 \hbox{}\qquad\qquad $P = \{a_2,\, a_3\}$ \\
1.24 @@ -370,7 +370,7 @@
1.25 \slshape Nitpick found no counterexample.
1.26 \postw
1.27
1.28 -Let's see if Sledgehammer \cite{sledgehammer-2009} can find a proof:
1.29 +Let's see if Sledgehammer can find a proof:
1.30
1.31 \prew
1.32 \textbf{sledgehammer} \\[2\smallskipamount]
1.33 @@ -552,7 +552,7 @@
1.34 cannot find a genuine counterexample for \textit{card~nat}~= $k$, it is very
1.35 unlikely that one could be found for smaller domains. (The $P~(\textit{op}~{+})$
1.36 example above is an exception to this principle.) Nitpick nonetheless enumerates
1.37 -all cardinalities from 1 to 8 for \textit{nat}, mainly because smaller
1.38 +all cardinalities from 1 to 10 for \textit{nat}, mainly because smaller
1.39 cardinalities are fast to handle and give rise to simpler counterexamples. This
1.40 is explained in more detail in \S\ref{scope-monotonicity}.
1.41
1.42 @@ -892,7 +892,7 @@
1.43 predicate evaluates to $\unk$. Thus, $\textit{even}'$ evaluates to either
1.44 \textit{True} or $\unk$, never \textit{False}.
1.45
1.46 -When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, and 24
1.47 +When unrolling a predicate, Nitpick tries 0, 1, 2, 4, 8, 12, 16, 20, 24, and 28
1.48 iterations. However, these numbers are bounded by the cardinality of the
1.49 predicate's domain. With \textit{card~nat}~= 10, no more than 9 iterations are
1.50 ever needed to compute the value of a \textit{nat} predicate. You can specify
1.51 @@ -1019,12 +1019,12 @@
1.52 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.53 \slshape The type ``\kern1pt$'a$'' passed the monotonicity test. Nitpick might be able to skip
1.54 some scopes. \\[2\smallskipamount]
1.55 -Trying 8 scopes: \\
1.56 +Trying 10 scopes: \\
1.57 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 1,
1.58 and \textit{bisim\_depth}~= 0. \\
1.59 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.60 -\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 8,
1.61 -and \textit{bisim\_depth}~= 7. \\[2\smallskipamount]
1.62 +\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} ``\kern1pt$'a~\textit{list\/}$''~= 10,
1.63 +and \textit{bisim\_depth}~= 9. \\[2\smallskipamount]
1.64 Nitpick found a counterexample for {\itshape card}~$'a$ = 2,
1.65 \textit{card}~``\kern1pt$'a~\textit{list\/}$''~= 2, and \textit{bisim\_\allowbreak
1.66 depth}~= 1:
1.67 @@ -1166,11 +1166,11 @@
1.68 \textbf{lemma}~``$\lnot\,\textit{loose}~t~0 \,\Longrightarrow\, \textit{subst}~\sigma~t = t$'' \\
1.69 \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
1.70 \slshape
1.71 -Trying 8 scopes: \nopagebreak \\
1.72 +Trying 10 scopes: \nopagebreak \\
1.73 \hbox{}\qquad \textit{card~nat}~= 1, \textit{card tm}~= 1, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 1; \\
1.74 \hbox{}\qquad \textit{card~nat}~= 2, \textit{card tm}~= 2, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 2; \\
1.75 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.76 -\hbox{}\qquad \textit{card~nat}~= 8, \textit{card tm}~= 8, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 8. \\[2\smallskipamount]
1.77 +\hbox{}\qquad \textit{card~nat}~= 10, \textit{card tm}~= 10, and \textit{card} ``$\textit{nat} \Rightarrow \textit{tm}$'' = 10. \\[2\smallskipamount]
1.78 Nitpick found a counterexample for \textit{card~nat}~= 6, \textit{card~tm}~= 6,
1.79 and \textit{card}~``$\textit{nat} \Rightarrow \textit{tm}$''~= 6: \\[2\smallskipamount]
1.80 \hbox{}\qquad Free variables: \nopagebreak \\
1.81 @@ -1193,14 +1193,14 @@
1.82 replaced with $\textit{lift}~(\sigma~m)~0$.
1.83
1.84 An interesting aspect of Nitpick's verbose output is that it assigned inceasing
1.85 -cardinalities from 1 to 8 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1.86 +cardinalities from 1 to 10 to the type $\textit{nat} \Rightarrow \textit{tm}$.
1.87 For the formula of interest, knowing 6 values of that type was enough to find
1.88 the counterexample. Without boxing, $46\,656$ ($= 6^6$) values must be
1.89 considered, a hopeless undertaking:
1.90
1.91 \prew
1.92 \textbf{nitpick} [\textit{dont\_box}] \\[2\smallskipamount]
1.93 -{\slshape Nitpick ran out of time after checking 4 of 8 scopes.}
1.94 +{\slshape Nitpick ran out of time after checking 4 of 10 scopes.}
1.95 \postw
1.96
1.97 {\looseness=-1
1.98 @@ -1221,7 +1221,7 @@
1.99 exhaust all models below a certain cardinality bound, the number of scopes that
1.100 Nitpick must consider increases exponentially with the number of type variables
1.101 (and \textbf{typedecl}'d types) occurring in the formula. Given the default
1.102 -cardinality specification of 1--8, no fewer than $8^4 = 4096$ scopes must be
1.103 +cardinality specification of 1--10, no fewer than $10^4 = 10\,000$ scopes must be
1.104 considered for a formula involving $'a$, $'b$, $'c$, and $'d$.
1.105
1.106 Fortunately, many formulas exhibit a property called \textsl{scope
1.107 @@ -1235,8 +1235,8 @@
1.108 \postw
1.109
1.110 where \textit{xs} is of type $'a~\textit{list}$ and \textit{ys} is of type
1.111 -$'b~\textit{list}$. A priori, Nitpick would need to consider 512 scopes to
1.112 -exhaust the specification \textit{card}~= 1--8. However, our intuition tells us
1.113 +$'b~\textit{list}$. A priori, Nitpick would need to consider $1\,000$ scopes to
1.114 +exhaust the specification \textit{card}~= 1--10. However, our intuition tells us
1.115 that any counterexample found with a small scope would still be a counterexample
1.116 in a larger scope---by simply ignoring the fresh $'a$ and $'b$ values provided
1.117 by the larger scope. Nitpick comes to the same conclusion after a careful
1.118 @@ -1248,7 +1248,7 @@
1.119 The types ``\kern1pt$'a$'' and ``\kern1pt$'b$'' passed the monotonicity test.
1.120 Nitpick might be able to skip some scopes.
1.121 \\[2\smallskipamount]
1.122 -Trying 8 scopes: \\
1.123 +Trying 10 scopes: \\
1.124 \hbox{}\qquad \textit{card} $'a$~= 1, \textit{card} $'b$~= 1,
1.125 \textit{card} \textit{nat}~= 1, \textit{card} ``$('a \times {'}b)$
1.126 \textit{list\/}''~= 1, \\
1.127 @@ -1260,11 +1260,11 @@
1.128 \hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 2, and
1.129 \textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 2. \\
1.130 \hbox{}\qquad $\qquad\vdots$ \\[.5\smallskipamount]
1.131 -\hbox{}\qquad \textit{card} $'a$~= 8, \textit{card} $'b$~= 8,
1.132 -\textit{card} \textit{nat}~= 8, \textit{card} ``$('a \times {'}b)$
1.133 -\textit{list\/}''~= 8, \\
1.134 -\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 8, and
1.135 -\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 8.
1.136 +\hbox{}\qquad \textit{card} $'a$~= 10, \textit{card} $'b$~= 10,
1.137 +\textit{card} \textit{nat}~= 10, \textit{card} ``$('a \times {'}b)$
1.138 +\textit{list\/}''~= 10, \\
1.139 +\hbox{}\qquad\quad \textit{card} ``\kern1pt$'a$ \textit{list\/}''~= 10, and
1.140 +\textit{card} ``\kern1pt$'b$ \textit{list\/}''~= 10.
1.141 \\[2\smallskipamount]
1.142 Nitpick found a counterexample for
1.143 \textit{card} $'a$~= 5, \textit{card} $'b$~= 5,
1.144 @@ -1281,7 +1281,7 @@
1.145 In theory, it should be sufficient to test a single scope:
1.146
1.147 \prew
1.148 -\textbf{nitpick}~[\textit{card}~= 8]
1.149 +\textbf{nitpick}~[\textit{card}~= 10]
1.150 \postw
1.151
1.152 However, this is often less efficient in practice and may lead to overly complex
1.153 @@ -1312,9 +1312,9 @@
1.154 \S\ref{inductive-datatypes}, \textit{nat}, \textit{int}, and inductive datatypes
1.155 are normally monotonic and treated as such. The same is true for record types,
1.156 \textit{rat}, \textit{real}, and some \textbf{typedef}'d types. Thus, given the
1.157 -cardinality specification 1--8, a formula involving \textit{nat}, \textit{int},
1.158 +cardinality specification 1--10, a formula involving \textit{nat}, \textit{int},
1.159 \textit{int~list}, \textit{rat}, and \textit{rat~list} will lead Nitpick to
1.160 -consider only 8~scopes instead of $32\,768$.
1.161 +consider only 10~scopes instead of $10\,000$.
1.162
1.163 \subsection{Inductive Properties}
1.164 \label{inductive-properties}
1.165 @@ -1658,7 +1658,7 @@
1.166 ``$w \in A \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] + 1$'' \\
1.167 ``$w \in B \longleftrightarrow \textit{length}~[x \mathbin{\leftarrow} w.\; x = b] = \textit{length}~[x \mathbin{\leftarrow} w.\; x = a] + 1$'' \\
1.168 \textbf{nitpick} \\[2\smallskipamount]
1.169 -\slshape Nitpick ran out of time after checking 7 of 8 scopes.
1.170 +\slshape Nitpick ran out of time after checking 7 of 10 scopes.
1.171 \postw
1.172
1.173 \subsection{AA Trees}
1.174 @@ -1767,7 +1767,7 @@
1.175 ``$\textit{dataset}~(\textit{skew}~t) = \textit{dataset}~t$'' \\
1.176 ``$\textit{dataset}~(\textit{split}~t) = \textit{dataset}~t$'' \\
1.177 \textbf{nitpick} \\[2\smallskipamount]
1.178 -{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.179 +{\slshape Nitpick ran out of time after checking 7 of 10 scopes.}
1.180 \postw
1.181
1.182 Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
1.183 @@ -1829,7 +1829,7 @@
1.184 \prew
1.185 \textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
1.186 \textbf{nitpick} \\[2\smallskipamount]
1.187 -{\slshape Nitpick ran out of time after checking 7 of 8 scopes.}
1.188 +{\slshape Nitpick ran out of time after checking 7 of 10 scopes.}
1.189 \postw
1.190
1.191 Insertion should transform the set of elements represented by the tree in the
1.192 @@ -1839,7 +1839,7 @@
1.193 \textbf{theorem} \textit{dataset\_insort\/}:\kern.4em
1.194 ``$\textit{dataset}~(\textit{insort}~t~x) = \{x\} \cup \textit{dataset}~t$'' \\
1.195 \textbf{nitpick} \\[2\smallskipamount]
1.196 -{\slshape Nitpick ran out of time after checking 6 of 8 scopes.}
1.197 +{\slshape Nitpick ran out of time after checking 6 of 10 scopes.}
1.198 \postw
1.199
1.200 We could continue like this and sketch a complete theory of AA trees. Once the
1.201 @@ -1984,7 +1984,7 @@
1.202 {\small See also \textit{box} (\S\ref{scope-of-search}) and \textit{mono}
1.203 (\S\ref{scope-of-search}).}
1.204
1.205 -\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{8}$}
1.206 +\opdefault{card}{int\_seq}{$\mathbf{1}$--$\mathbf{10}$}
1.207 Specifies the default sequence of cardinalities to use. This can be overridden
1.208 on a per-type basis using the \textit{card}~\qty{type} option described above.
1.209
1.210 @@ -2032,7 +2032,7 @@
1.211 {\small See also \textit{bits} (\S\ref{scope-of-search}) and
1.212 \textit{show\_datatypes} (\S\ref{output-format}).}
1.213
1.214 -\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
1.215 +\opdefault{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12},\mathbf{14},\mathbf{16}$}
1.216 Specifies the number of bits to use to represent natural numbers and integers in
1.217 binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
1.218
1.219 @@ -2082,12 +2082,12 @@
1.220 {\small See also \textit{wf} (\S\ref{scope-of-search}) and
1.221 \textit{star\_linear\_preds} (\S\ref{optimizations}).}
1.222
1.223 -\opdefault{iter}{int\_seq}{$\mathbf{1{,}2{,}4{,}8{,}12{,}16{,}24{,}32}$}
1.224 +\opdefault{iter}{int\_seq}{$\mathbf{0{,}1{,}2{,}4{,}8{,}12{,}16{,}20{,}24{,}28}$}
1.225 Specifies the sequence of iteration counts to use when unrolling (co)in\-duc\-tive
1.226 predicates. This can be overridden on a per-predicate basis using the
1.227 \textit{iter} \qty{const} option above.
1.228
1.229 -\opdefault{bisim\_depth}{int\_seq}{$\mathbf{7}$}
1.230 +\opdefault{bisim\_depth}{int\_seq}{$\mathbf{9}$}
1.231 Specifies the sequence of iteration counts to use when unrolling the
1.232 bisimilarity predicate generated by Nitpick for coinductive datatypes. A value
1.233 of $-1$ means that no predicate is generated, in which case Nitpick performs an
1.234 @@ -2454,7 +2454,7 @@
1.235 together ensures that Kodkodi is launched less often, but it makes the verbose
1.236 output less readable and is sometimes detrimental to performance. If
1.237 \textit{batch\_size} is set to \textit{smart}, the actual value used is 1 if
1.238 -\textit{debug} (\S\ref{output-format}) is set and 64 otherwise.
1.239 +\textit{debug} (\S\ref{output-format}) is set and 50 otherwise.
1.240
1.241 \optrue{destroy\_constrs}{dont\_destroy\_constrs}
1.242 Specifies whether formulas involving (co)in\-duc\-tive datatype constructors should
1.243 @@ -2629,13 +2629,17 @@
1.244 equationally).
1.245 \item[2.] If the definition is of the form
1.246
1.247 -\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$,
1.248 -
1.249 -then Nitpick assumes that the definition was made using an inductive package
1.250 -based on the introduction rules registered in Isabelle's internal
1.251 -\textit{Spec\_Rules} table. It uses the introduction rules to ascertain whether
1.252 -the definition is well-founded and the definition to generate a fixed-point
1.253 -equation or an unrolled equation.
1.254 +\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
1.255 +
1.256 +or
1.257 +
1.258 +\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t)$
1.259 +
1.260 +Nitpick assumes that the definition was made using a (co)inductive package
1.261 +based on the user-specified introduction rules registered in Isabelle's internal
1.262 +\textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
1.263 +whether the definition is well-founded and the definition to generate a
1.264 +fixed-point equation or an unrolled equation.
1.265 \end{enum}
1.266 \end{enum}
1.267