Closed racket-bug-submit closed 12 years ago
Rex, this is not a bug. The random testing defproperty performs at
runtime neither guarantees the logical truth of a claim, nor aids
ACL2's proof search. There are many defproperty terms that run
successfully but nevertheless will not admit. To find the problem,
you'll have to either find a counterexample by refining the random
distributions or prove the theorem correct by applying normal ACL2
techniques.
--Carl
On Wed, Oct 29, 2008 at 6:56 PM, <page@ou.edu> wrote:
> A new problem report is waiting at
> http://bugs.plt-scheme.org/query/?cmd=view&pr=9876
>
> Reported by Rex Page for release: 4.1
>
> *** Description:
> Property definitions usually admit under the ACL2 mode in Dracula, but there seems to be at least one case where a runnable property fails to admit
DoubleCheck's random testing does not guarantee successful theorem proving.
Dracula.
Not a bug.
Originally submitted on: Wed Oct 29 18:56:01 -0400 2008
Steps to Reproduce:
Release:
4.1
Environment:
windows "Windows NT 5.1 (Build 2600) Service Pack 3" (win32\i386\3m) (get-display-depth) = 32 Human Language: english (current-memory-use) 98983816
Collections: (("C:\Documents and Settings\Rex Page\Application Data\PLT Scheme\4.1\collects" non-existent-path) ("C:\Program Files\PLT\collects" "afm" "algol60" "browser" "combinator-parser" "compiler" "config" "defaults" "drscheme" "dynext" "embedded-gui" "eopl" "errortrace" "ffi" "file" "framework" "frtime" "games" "graphics" "gui-debugger" "help" "hierlist" "htdch" "htdp" "html" "icons" "info-domain" "lang" "launcher" "lazy" "macro-debugger" "make" "mred" "mrlib" "mysterx" "mzcom" "mzlib" "mzscheme" "net" "openssl" "parser-tools" "planet" "plot" "preprocessor" "profj" "r5rs" "r6rs" "readline" "redex" "rnrs" "s-exp" "scheme" "scribble" "scribblings" "setup" "sgl" "slatex" "slideshow" "srfi" "stepper" "string-constants" "swindle" "syntax" "syntax-color" "teachpack" "test-box-recovery" "test-engine" "tex2page" "texpict" "trace" "typed-scheme" "version" "web-server" "wxme" "xml")) Computer Language: (("Dracula Languages" "Dracula v4.2") (#("C:\ACL2-3.3\bin\acl2.exe" #f) . #(#t write mixed-fraction-e #f #t debug)))
This bug was converted from Gnats bug 9876.
[anon-submit page AT ou.edu]