ACM通信
新闻
正式的软件验证措施
来源:Class Central
现代世界是靠软件运行的。从智能手机和汽车到医疗设备和发电厂，可执行代码驱动洞察力和自动化。然而，有一个问题:计算机代码经常包含编程错误——有些小，有些大。这些小故障会导致意想不到的结果和系统故障。
“在很多情况下，软件缺陷不会造成任何影响。在其他情况下，它们可能会造成巨大的问题，”塔夫茨大学计算机科学系教授兼主席、美国国防高级研究计划局(DARPA)前官员凯瑟琳·费舍尔说。
评论
保罗·吉布森
规范“对于0 <= j < k < N的所有值j和k，必须是B[i] < B[j].”定义了索引j和k，但使用了索引i和j。如果初始数组包含相等的元素也是有问题的。这些不仅仅是不完整的问题。
劳伦斯Markosian
TLA+的发明者是Leslie Lamport, 2013年ACM图灵奖得主:
“对分布式和并发系统的理论和实践做出了基本贡献，特别是发明了因果关系和逻辑时钟、安全性和活性、复制状态机和顺序一致性等概念。”Lamport的网站，lamport.org，讨论了TLA+及其一些工业应用。
塞缪尔·格林加德
感谢J. Paul和Lawrence的评论。我很感谢你指出这些事情，尤其是莱斯利·兰波特的贡献。
显示3评论