formal-verification

    1热度

    1回答

    细化B型规范

    的考虑我在B型规范如下： - flower <: FLOWER age <: AGE owner <: OWNER Type <: flower * age Buyer : owner <-> flower 是否有可能对我来说，随后创建一个细化： - flower <: FLOWER age <: AGE owner <: OWNER Type : Owner <-> flowe
    formal-verification formal-methods refinement-type b-method 2017-07-19

    1热度

    1回答

    如何在精益中使用Pi类型编写非相关产品的定义？

    我正在努力通过“定理证明在精益中”的chapter 7 – Inductive Types。 我想知道如何编写 依赖非独立产品的定义在更多扩展或“原始”形式。 它看起来像在自动教程中给出的定义推断一些细节： inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1 一些实验允许填写详细 inductive prod2 (α : T
    dependent-type theorem-proving formal-verification lean 2017-07-29

    2热度

    1回答

    使用SPIN进行LTL模型检查

    我正在查看SPIN软件。我想用它来找到LTL理论的模型。所有的手册和教程讨论验证算法的属性，但我根本不感兴趣。我只想找到LTL公式的模型（我猜想是相应的Büchi自动机），就像mace4或paradox模型检测器可以找到FOL公式的模型。我相信SPIN应该能够做到这一点，但我无法在文档中找到它。有人能指出任何有用的资源吗？
    logic formal-verification model-checking spin promela 2017-08-02

    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
    dependent-type formal-verification lean 2017-08-11

    3热度

    1回答

    SMT解决方案与自定义理论？

    我在做一些验证工作，我已经将常规树语法作为基础理论。 Z3允许您定义自己的东西与未解释的函数，但是，如果您的决策过程是递归的，那么这种方法并不适用。他们曾经允许使用插件，但我认为这已经被删除了。 我想知道，有没有人有一个体面的SMT解决方案的建议，让你写定制理论的决策程序？
    z3 verification smt formal-verification sat 2017-10-01

    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
    dependent-type theorem-proving formal-verification lean 2017-08-13

    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
    formal-verification loop-invariant dafny 2017-06-26

    1热度

    1回答

    定义精益自然数的前驱函数（pred 0 = 0）

    我正在学习精益证明助手。 https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html的练习是为自然数定义前驱函数。有人可以帮助我吗？
    dependent-type formal-verification lean 2017-10-08

    1热度

    1回答

    测试多项式定义（从自然数到整数）

    对于我的第一次正式化。我想在精益中定义多项式。 第一次尝试如下： def polynomial (f : ℕ → ℤ ) (p: (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (f n = (0:ℤ) ))):= f 现在想用测试我的定义： def test : ℕ → ℤ | 0 := (2:ℤ) | 1 := (3:ℤ) | 2 := (4:ℤ) | _ := (0
    dependent-type formal-verification lean 2017-10-19

    8热度

    1回答

    证明继承人超越平等的替代财产

    我试图从chapter 7 of "theorem proving in lean"了解归纳类型。 我给自己设定了证明自然数的是继任者的任务，拥有平等的一个替代性质： inductive natural : Type | zero : natural | succ : natural -> natural lemma succ_over_equality (a b : natural) (
    dependent-type theorem-proving formal-verification lean 2017-07-17
最新问题