我试图在ACL2s/Lisp中证明这个函数,但它返回一个堆栈溢出错误,虽然我看不到代码中的缺陷.
(defunc foo (x y) :input-contract (and (natp x) (natp y)) :output-contract (natp (foo x y)) (cond ((equal 0 x) (+ y 1)) ((equal 0 y) (foo (- x 1) 1)) (t (foo (- x 1) (foo x (+ y 1))))))
zck.. 5
那不是任何积极x
和y
造成这种溢出?我们来看看吧(foo 1 1)
.
既不是x
也不y
是零,所以它到达t
cond 的分支,并调用:
(foo 0 (foo 1 2))
好吧,让我们评估一下内部foo
呼叫:
(foo 1 2)
同样,它到达t
cond 的分支,并调用:
(foo 0 (foo 1 3))
让我们评估内心foo
:
(foo 1 3)
你可以看到它的发展方向.该t
分公司电话:
(foo 0 (foo 1 4))
等等.这将在任何时候发生x
,y
并且非零.你从哪里得到这段代码?你想用它做什么?运行它也是一个好主意,看看溢出了什么.在这种情况下,几乎每个可能的调用都会出现堆栈溢出.
那不是任何积极x
和y
造成这种溢出?我们来看看吧(foo 1 1)
.
既不是x
也不y
是零,所以它到达t
cond 的分支,并调用:
(foo 0 (foo 1 2))
好吧,让我们评估一下内部foo
呼叫:
(foo 1 2)
同样,它到达t
cond 的分支,并调用:
(foo 0 (foo 1 3))
让我们评估内心foo
:
(foo 1 3)
你可以看到它的发展方向.该t
分公司电话:
(foo 0 (foo 1 4))
等等.这将在任何时候发生x
,y
并且非零.你从哪里得到这段代码?你想用它做什么?运行它也是一个好主意,看看溢出了什么.在这种情况下,几乎每个可能的调用都会出现堆栈溢出.