Logic

一行代码都不运行，为什么能证明程序“绝对没有Bug”？形式化验证与模型检测的科学