如何使用「undefined」常量驗證代碼正確性引理

鑑於我有一個非常簡單的代碼生成定義。它僅在某些情況下被定義，否則會引發運行時異常。如何使用「undefined」常量驗證代碼正確性引理

definition "blubb a = (if P a then True else undefined)"

現在我想顯示blubb正確。應該忽略拋出異常的情況（從我的觀點來看，不是數學觀點）。然而，我最終得到一個子目標，它假設X是undefined的一些任意值。下面的引理或多或少地等同於子目標。我想顯示False，因爲我想忽略拋出異常的情況（即，返回undefined）。

lemma "X = undefined ⟹ False"

這是不可證明的。

try 

Nitpick found a counterexample for card 'a = 1: 
Free variable: 
    X = a1

什麼是展示的功能正確性可能會拋出異常錯誤或處理undefined的最佳方式？這涉及到this的問題。

來源

2013-03-20 corny

通過顯示「blubb」正確，你的意思是什麼？對我而言，這只是'P == ==> blubb'，這對於給定的定義來說是微不足道的。 – chris 2013-03-20 02:41:05

'blubb'就是一個例子。例如，'blubb a'可能是一種有效的算法，可以比默認實現更快地計算'distinct a'，但只是爲排序列表定義的（壞例子）...... – corny 2013-03-20 13:11:45

undefined在Isabelle中是一個常數，你對此一無所知。特別是，你一般不能證明X ≠ undefined。

如果你想寫一個僅適用於特定輸入功能，您可以考慮使用'a option類型，如下所示：

definition "blubb a ≡ (if P a then Some True else None)"

，然後在你的證明假設blubb a定義如下：

lemma "∃x. blubb a = Some x ⟹ Q (blubb a)" 
    ...

或者乾脆：

lemma "a ∈ dom blubb ⟹ Q (blubb a)" 
    ...

然後可以使用the (blubb a)來提取blubb a的值。

來源

2013-03-20 01:27:18 davidg

有些情況下可以顯示** **等於'undefined'。例如，在'〜P a ==> blubb a = undefined'之上可以工作。顯示一些'X'是**不等於'undefined'將永遠不會工作（因爲'undefined'是'X'類型的任意居民，因此**可能確實是'X';這種建築工程，因爲'HOL'中的每種類型都有人居住）。 – chris 2013-03-20 02:48:39

@chris：好點。我試圖澄清我的答案。 – davidg 2013-03-20 03:08:26

如果我真的對代碼生成感興趣並且不想要一個選項類型，而是拋出一個異常而不是'None'？ – corny 2013-03-20 13:13:12

如何使用「undefined」常量驗證代碼正確性引理

回答

相關問題