软件的设计过程就是一个建立形式规约的过程。
当规格说明用非形式化方法说明时，可称之为“规格说明”，当用形式化方法说明时，可称之为“形式规约”。已建立的形式化方法可分为操作类和描述类。形式证明与验证技术主要包括模型检测和定理证明，模型检测主要适用于有穷状态系统，优点是完全自动化并且验证速度快，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。程序求精是将一个抽象程度低、过程性强的程序替代一个抽象程度高、过程性低的程序。当规格说明用非形式化方法说明时，可称之为“规格
阅读背景：
软件工程—第五章—软件工程中的形式化方法
来源：互联网
分享到：
