L1-introduction

1，软件验证意味着证明一个软件是正确的（它会做它应该做的事情） specification：一个关于这个程序应该做什么的声明。 Formal specification：用某种正式语言编写的程序应该做什么的声明。 程序测试可以用来显示错误的存在，但永远不能显示它们的缺失！、

Software Verification means proving that a piece of software is correct The specification is a statement of what the program is supposed to do

2，软件验证是 基于对形式方法的研究：程序的规范、建模、构建和验证 建立在逻辑和自动机理论的基础上，与计算理论和编程语言的形式语义密切相关