【问题标题】:Soundness and completeness of systems系统的健全性和完整性
【发布时间】:2014-02-21 14:33:04
【问题描述】:

首先是一些术语(借自here,第14页):

肯定的程序是有错误的程序。

否定程序是没有错误的程序。


所以有四种类型的程序:

阳性程序,分析为阳性 -> 真阳性 (TP)。

阳性程序,分析为阴性 -> 假阴性 (FN)。

一个否定程序,分析为肯定 -> 误报 (FP)。

一个否定程序,分析为否定 -> 真否定 (TN)。


一个系统是健全的,如果它从不接受一个积极的程序。

一个系统是完整的,如果它从不拒绝否定程序。


所以从我上面写的来看:
A complete system accepts FN and TN programs.
A sound system also accepts FN and TN programs.

一位同事告诉我,音响系统也接受 FP 程序。有人可以证实这一点并解释他们为什么这样做吗?

【问题讨论】:

    标签: logic theory type-systems


    【解决方案1】:

    这本书是这样解释的:

    健全性可防止误报,完整性可防止误报。

    因此,为了使系统健全,它不需要防止误报,而只需防止误报。为了防止误报,它必须是完整的。

    本书以类型系统为例进一步解释:

    在现代语言中,类型系统是健全的(它们阻止了它们声称的)但不是完整(它们 拒绝他们不需要拒绝的程序)。健全性很重要,因为它让语言用户和语言 实施者依赖 X 永远不会发生。完整性会很好,但希望在实践中很少见 一个程序被不必要地拒绝了,在这些情况下,希望程序员很容易修改 程序进行类型检查。

    类型系统并不完整,因为几乎所有您可能想静态检查的东西都是不可能的 实现一个静态检查器,给定您的语言中的任何程序(a)总是终止,(b)是健全的, (c) 是完整的。既然我们必须放弃一个,(c)似乎是最好的选择(程序员不喜欢 可能不会终止的编译器)。

    【讨论】:

      【解决方案2】:

      假设房主设置了警报系统来检测小偷。业主不喜欢由于非法入侵以外的其他原因而误报警,这会使系统变得不那么敏感,在这种情况下,当警报响起时,就意味着“警报意味着有入侵者”,存在无法检测到熟练窃贼的危险。可以忍受虚惊但从不希望入侵的细心和谨慎的所有者可能会使系统更加敏感。在这种情况下,“没有警报意味着没有入侵”。

      第一个不接受误报(在本例中为误报)的系统称为声音系统,这意味着不存在类型 1 错误。第二个永远不会错过入侵的系统,换句话说,永远不会接受假阴性,称为完整系统,这意味着不存在类型 2 错误。健全并不能保证完整性,反之亦然。具有完善的报警系统灵敏度,无误报警,无漏报入侵,使系统健全完整。

      此页面 (http://ubccpsc311.blogspot.jp/2010/11/7-ways-to-approach-soundness-and.html) 给出了关于健全性和完整性的七个观点。另请参阅Soundness and Completeness of a algorithm,它表示当健全的算法从不给出错误答案(从不返回错误结果)时,完整算法总能找到答案。这个https://softwareengineering.stackexchange.com/questions/140705/what-does-it-mean-to-say-an-algorithm-is-sound-and-complete 也可能有帮助。

      An Integrated approach to software engineering 的内容展示了静态分析器示例的另一个视角。

      在书中soundness captures the occurrence of false positives,换句话说,有了完美的声音系统,当它们实际上是警告时没有错误报告:less soundness implies more false positives

      话虽如此,我认为作者的评论可能是一个错字,应该写成“健全性防止误报......”。可能,在作者的领域中,健全性意味着与通常使用的不同,但我不确定。

      理解这些定义的一个好方法是,健全性可以防止 漏报和完整性可防止误报。

      另外,我认为OP的评论也令人困惑:

      A system is sound, if it never accepts a positive program.
      A system is complete, if it never rejects a negative program.
      

      更好/正确的描述可能是

      A system is sound, if it never accepts a false positive program.
      A system is complete, if it never accepts a false negative program.
      

      【讨论】:

      • 这不是人们通常谈论健全性和完整性的方式。误报是被报告为阳性但实际上是阴性的东西。假阴性是被报告为阴性但实际上是阳性的东西。
      猜你喜欢
      • 2019-07-24
      • 1970-01-01
      • 1970-01-01
      • 1970-01-01
      • 2015-12-27
      • 1970-01-01
      • 2020-03-01
      • 1970-01-01
      • 1970-01-01
      相关资源
      最近更新 更多