2016-01-25 49 views
1

我試圖在ACL2(特別是ACL2s)中編寫一個函數,該函數接受列表和自然數並返回給定索引處列表中的項。所以(選擇(表1 2 3)2)將返回3.在ACL2中寫入select()函數

這裏是我的代碼:

;; 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)) 

任何幫助是多少不勝感激!

回答

1

該消息似乎很清楚:您試圖獲取空列表的第一個元素,這與您的規範衝突。

基於this reference,似乎first需要一個非空列表,而car回報nil當你輸入nil

要麼你明確地用endp測試來處理nil的情況,要麼你用car而不是first

+0

使用'endp'工作!我曾假設'第一'會接受一個非空列表,但我錯了。謝謝! – camden

+0

@camdenb我很高興它的工作,繼續前進:-) – coredump