1

リストと自然数を取り、指定されたインデックスでリスト内の項目を返す ACL2 (具体的には ACL2s) に関数を記述しようとしています。したがって、 (select (list 1 2 3) 2) は 3 を返します。

これが私のコードです：

;; select: List x Nat -> All
(defunc select (l n)
  :input-contract (and (listp l) (natp n))
  :output-contract t
  (if (equal 0 n)
    (first l)
    (select (rest l) (- n 1))))

次のエラーが表示されます。

Query: Testing body contracts ... 

**Summary of Cgen/testing**
We tested 50 examples across 1 subgoals, of which 48 (48 unique) satisfied
the hypotheses, and found 1 counterexamples and 47 witnesses.

We falsified the conjecture. Here are counterexamples:
 [found in : "top"]
 -- ((L NIL) (N 0))

Test? found a counterexample.
Body contract falsified in: 
 -- (ACL2::EXTRA-INFO '(:GUARD (:BODY SELECT)) '(FIRST L))

どんな助けでも大歓迎です！

4

1 に答える 1

1

メッセージは私にはかなり明確に思えます:空のリストの最初の要素を取得しようとしていますが、これは仕様と競合しています。

この参照に基づいてfirst、空でないリストが必要なようですが、入力が の場合にcar戻ります。nilnil

ケースをテストnilで明示的に処理するか、代わりにを使用します。endpcarfirst

于 2016-01-25T19:51:57.147 に答える