fbpx
维基百科

正确性 (计算机科学)

理论计算机科学中,算法的正确性(英语:correctness)是指一个算法在程序规范下被认定为正确的判定。其中,功能正确(英语:functional correctness)针对输入输出的行为(例如:对每一个输入,算法都能给出预期的输出)。[1]

人们将正确性分为两类。一类被称为部分正确性(英语:partial correctness),它要求在算法返回结果时这一结果是正确的;另一类被称为完全正确性(英语:total correctness),它在部分正确性的基础之上还要求算法必须能够结束。由于对于停机问题没有通用的解决方案,因此判定完全正确性的断言有着更多需要深层次研究的地方。终止的证明是指一类数学证明,因为完全正确性需要证明一个算法会终止,所以它在程序的形式验证中起着至关重要的作用。[2]

例如考虑这样一个问题:依次搜索整数列1, 2, 3, …来看是否存在某个特定现象——比如说存在一个奇数为完全数。对于这个问题而言,我们很容易写出一个部分正确的程序(直接对于每个数字做长除法判定其是否完全)。然而如果我们想证明这个程序是完全正确的,那就相当于我们在断言一个在数论目前还未知的结论

在算法和程序规范都是基于形式化来给出时,对正确性的证明应当为一个数学证明。然而我们并不期待能够给出特定机器上实现的特定程序的正确性断言,因为那样将需要考虑诸如内存限制在内的更多问题。

证明论中有一个结论柯里-霍华德同构。这一结论认为:任意一个在构造性逻辑下的功能正确性的证明都对应了一个λ演算程序。这种转换证明的方式被称为程序抽出(英文:program extraction)。

霍尔逻辑是一个具体的能够严密验证程序正确性的形式系统[3]它用一系列的公理来定义程序语言的语义,从而通过称之为霍尔三元组的断言来验证程序的正确性。

软件测试是指验证一个程序或系统的某些属性或能力来判断它是否达到预期目的的行为。尽管软件测试在软件质量方面起着至关重要的作用,并且被程序员和测试员们广泛采用,但由于人们对软件的认识十分有限,它仍旧是一个艰深的领域。软件测试的最大难点在于如何控制其复杂性:我们没有办法在一个合理的复杂度内完整地测试一个程序。测试不只是调试。测试的目的包括但不限于确保软件质量、验证其正确性和估算其稳定性。我们对测试的定义也可以更加一般化,其中正确性测试和稳定性测试是两个最大的研究领域。软件测试是预算、时间和软件质量的一个平衡。[4]

参见 编辑

注释 编辑

  1. ^ Dunlop, Douglas D.; Basili, Victor R. A Comparative Analysis of Functional Correctness. ACM通讯. June 1982, 14 (2): 229–244. doi:10.1145/356876.356881. 
  2. ^ Manna, Zohar; Pnueli, Amir. Axiomatic approach to total correctness of programs (PDF). Acta Informatica. September 1974, 3 (3): 243–263. doi:10.1007/BF00288637. 
  3. ^ Hoare, C. A. R. (PDF). ACM通讯. October 1969, 12 (10): 576–580. doi:10.1145/363235.363259. (原始内容 (PDF)存档于4 March 2016). 
  4. ^ Pan, Jiantao. (coursework). Carnegie Mellon University. Spring 1999 [21 November 2017]. (原始内容存档于2009-12-25). 

参考资料 编辑

  • "Human Language Technology. Challenges for Computer Science and Linguistics." Google Books. N.p., n.d. Web. 2017年4月10日
  • "Security in Computing and Communications." Google Books. N.p., n.d. Web. 2017年4月10日
  • "The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation." The Halting Problem of Alan Turing - A Most Merry and Illustrated Explanation. N.p., n.d. Web. 2017年4月10日.
  • Turner, Raymond, and Nicola Angius. "The Philosophy of Computer Science." Stanford Encyclopedia of Philosophy. 斯坦福大学, 2013年8月20日. Web. 2017年4月10日.
  • Dijkstra, E. W. Program Correctness. Austin, Texas?: U of Texas at Austin, Departments of Mathematics and Computer Sciences, Automatic Theorem Proving Project?, 1970. Web.

正确性, 计算机科学, 此條目翻譯自其他語言維基百科, 需要相關領域的編者協助校對翻譯, 如果您精通本領域, 又能清楚地將來源語言翻譯為中文, 歡迎您協助校訂翻譯, 原文参见维基数据, 在理论计算机科学中, 算法的正确性, 英语, correctness, 是指一个算法在程序规范下被认定为正确的判定, 其中, 功能正确, 英语, functional, correctness, 针对输入输出的行为, 例如, 对每一个输入, 算法都能给出预期的输出, 人们将正确性分为两类, 一类被称为部分正确性, 英语, parti. 此條目翻譯自其他語言維基百科 需要相關領域的編者協助校對翻譯 如果您精通本領域 又能清楚地將來源語言翻譯為中文 歡迎您協助校訂翻譯 原文参见维基数据 在理论计算机科学中 算法的正确性 英语 correctness 是指一个算法在程序规范下被认定为正确的判定 其中 功能正确 英语 functional correctness 针对输入输出的行为 例如 对每一个输入 算法都能给出预期的输出 1 人们将正确性分为两类 一类被称为部分正确性 英语 partial correctness 它要求在算法返回结果时这一结果是正确的 另一类被称为完全正确性 英语 total correctness 它在部分正确性的基础之上还要求算法必须能够结束 由于对于停机问题没有通用的解决方案 因此判定完全正确性的断言有着更多需要深层次研究的地方 终止的证明是指一类数学证明 因为完全正确性需要证明一个算法会终止 所以它在程序的形式验证中起着至关重要的作用 2 例如考虑这样一个问题 依次搜索整数列1 2 3 来看是否存在某个特定现象 比如说存在一个奇数为完全数 对于这个问题而言 我们很容易写出一个部分正确的程序 直接对于每个数字做长除法判定其是否完全 然而如果我们想证明这个程序是完全正确的 那就相当于我们在断言一个在数论里目前还未知的结论 在算法和程序规范都是基于形式化来给出时 对正确性的证明应当为一个数学证明 然而我们并不期待能够给出特定机器上实现的特定程序的正确性断言 因为那样将需要考虑诸如内存限制在内的更多问题 证明论中有一个结论柯里 霍华德同构 这一结论认为 任意一个在构造性逻辑下的功能正确性的证明都对应了一个l演算程序 这种转换证明的方式被称为程序抽出 英文 program extraction 霍尔逻辑是一个具体的能够严密验证程序正确性的形式系统 3 它用一系列的公理来定义程序语言的语义 从而通过称之为霍尔三元组的断言来验证程序的正确性 软件测试是指验证一个程序或系统的某些属性或能力来判断它是否达到预期目的的行为 尽管软件测试在软件质量方面起着至关重要的作用 并且被程序员和测试员们广泛采用 但由于人们对软件的认识十分有限 它仍旧是一个艰深的领域 软件测试的最大难点在于如何控制其复杂性 我们没有办法在一个合理的复杂度内完整地测试一个程序 测试不只是调试 测试的目的包括但不限于确保软件质量 验证其正确性和估算其稳定性 我们对测试的定义也可以更加一般化 其中正确性测试和稳定性测试是两个最大的研究领域 软件测试是预算 时间和软件质量的一个平衡 4 参见 编辑形式验证 契约式设计 程序分析 模型验证 编译器正确性 程序派生注释 编辑 Dunlop Douglas D Basili Victor R A Comparative Analysis of Functional Correctness ACM通讯 June 1982 14 2 229 244 doi 10 1145 356876 356881 Manna Zohar Pnueli Amir Axiomatic approach to total correctness of programs PDF Acta Informatica September 1974 3 3 243 263 doi 10 1007 BF00288637 Hoare C A R An axiomatic basis for computer programming PDF ACM通讯 October 1969 12 10 576 580 doi 10 1145 363235 363259 原始内容 PDF 存档于4 March 2016 Pan Jiantao Software Testing coursework Carnegie Mellon University Spring 1999 21 November 2017 原始内容存档于2009 12 25 参考资料 编辑 Human Language Technology Challenges for Computer Science and Linguistics Google Books N p n d Web 2017年4月10日 Security in Computing and Communications Google Books N p n d Web 2017年4月10日 The Halting Problem of Alan Turing A Most Merry and Illustrated Explanation The Halting Problem of Alan Turing A Most Merry and Illustrated Explanation N p n d Web 2017年4月10日 Turner Raymond and Nicola Angius The Philosophy of Computer Science Stanford Encyclopedia of Philosophy 斯坦福大学 2013年8月20日 Web 2017年4月10日 Dijkstra E W Program Correctness Austin Texas U of Texas at Austin Departments of Mathematics and Computer Sciences Automatic Theorem Proving Project 1970 Web 取自 https zh wikipedia org w index php title 正确性 计算机科学 amp oldid 75010986, 维基百科,wiki,书籍,书籍,图书馆,

文章

,阅读,下载,免费,免费下载,mp3,视频,mp4,3gp, jpg,jpeg,gif,png,图片,音乐,歌曲,电影,书籍,游戏,游戏。