软件工程中的形式化方法

软件工程中的形式化方法，软件规格说明是对软件系统对象，对象的操作方法，以及对象行为的描述。在系统的开发及演化过程中，对象、对象的性质以及操作应作为一个整体来处理。形式证明与实验技术主要包括模型检测和定理证明。程序求精是将自动推理和形式化方法相结合，从抽象的形式规约推演出具体的面向计算机的程序代码的全过程。模态逻辑通过引入“可能”和“必然”两个模态词，从而对可能世界中的命题进行描述和演算。标记算法是模型检验的一个简单算法。