形式化技术在大型软件工程中的作用

20多年前,人们断言:软件产品的规模和目标将因程序的可靠性难以保证而受到严重的限制。一些评论家严厉指出,专业人员所编制的程序中,每千行程序代码会包含10个以内独立的可改正的错误。对整个软件而言,原则上说,错误的程序代码会带来不理想的结果,甚至引入歧途。有人警告说:在一些由计算机系统控制,同时需要绝对安全的领域,如医疗设备、军事武器甚至包括核反应堆,这些危险同样存在。这些观点促使我们投入主要的精力去研究一项重要课题——程序的正确性。