证件检查的程序

    研究程序正确性的理论。为了解一个程序是否正确地实现了预定的目标，通常是规定一些初始数据，试验性地执行这个程序，测试其是否能产生所要的答案。如果发现有误，就检查和修改所编的程序，直至对所有规定的初始数据，都能产生预期的结果。这种方法称为程序调试。但是，程序对不同的初始数据的加工过程是不同的，而初始数据的取值范围往往又十分广泛。因此，使用调试方法穷尽程序的各种可能加工过程以确保程序的正确性，几乎是不可能实现的。因此，调试方法只能发现程序的错误，而不能确保程序无误。程序验证则是研究如何使用数学方法严格证明一个程序是符合其预定的目标的，因而是正确无误的。