formal-verification

1熱度

1回答

的考慮我在B型規範如下： - flower <: FLOWER age <: AGE owner <: OWNER Type <: flower * age Buyer : owner <-> flower 是否有可能對我來說，隨後創建一個細化： - flower <: FLOWER age <: AGE owner <: OWNER Type : Owner <-> flowe

1熱度

1回答

如何在精益中使用Pi類型編寫非相關產品的定義？

我正在努力通過「定理證明在精益中」的chapter 7 – Inductive Types。我想知道如何編寫依賴非獨立產品的定義在更多擴展或「原始」形式。它看起來像在自動教程中給出的定義推斷一些細節： inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1 一些實驗允許填寫詳細 inductive prod2 (α : T

2熱度

1回答

使用SPIN進行LTL模型檢查

我正在查看SPIN軟件。我想用它來找到LTL理論的模型。所有的手冊和教程討論驗證算法的屬性，但我根本不感興趣。我只想找到LTL公式的模型（我猜想是相應的Büchi自動機），就像mace4或paradox模型檢測器可以找到FOL公式的模型。我相信SPIN應該能夠做到這一點，但我無法在文檔中找到它。有人能指出任何有用的資源嗎？

1熱度

1回答

在精益中使用集合

我想用精益做一些拓撲工作。作爲一個好的開始，我想證明一些關於sets in lean的簡單引理。例如 def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B := sorry 或 def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (s

3熱度

1回答

SMT解決方案與自定義理論？

我在做一些驗證工作，我已經將常規樹語法作爲基礎理論。 Z3允許您定義自己的東西與未解釋的函數，但是，如果您的決策過程是遞歸的，那麼這種方法並不適用。他們曾經允許使用插件，但我認爲這已經被刪除了。我想知道，有沒有人有一個體面的SMT解決方案的建議，讓你寫定製理論的決策程序？

1熱度

1回答

從設置包含到設置精簡的平等

給定集合包含的證明及其相反，我希望能夠證明兩個集合是平等的。例如，我知道如何證明following statement，並its converse： open set universe u variable elem_type : Type u variable A : set elem_type variable B : set elem_type def set_deMorga

17熱度

1回答

用Dafny證明100個囚犯和一個燈泡

考慮解決100 prisoners and a lightbulb問題的標準策略。這是我嘗試它Dafny型號： method strategy<T>(P: set<T>, Special: T) returns (count: int) requires |P| > 1 && Special in P ensures count == (|P| - 1) decrea

1熱度

1回答

定義精益自然數的前驅函數（pred 0 = 0）

我正在學習精益證明助手。 https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html的練習是爲自然數定義前驅函數。有人可以幫助我嗎？

1熱度

1回答

測試多項式定義（從自然數到整數）

對於我的第一次正式化。我想在精益中定義多項式。第一次嘗試如下： def polynomial (f : ℕ → ℤ ) (p: (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (f n = (0:ℤ) ))):= f 現在想用測試我的定義： def test : ℕ → ℤ | 0 := (2:ℤ) | 1 := (3:ℤ) | 2 := (4:ℤ) | _ := (0

8熱度

1回答

證明繼承人超越平等的替代財產

我試圖從chapter 7 of "theorem proving in lean"瞭解歸納類型。我給自己設定了證明自然數的是繼任者的任務，擁有平等的一個替代性質： inductive natural : Type | zero : natural | succ : natural -> natural lemma succ_over_equality (a b : natural) (