形式化方法 形式化方法是指为说明和验证复杂计算机系统所 采用的基于数学的语言、技术和工具。 ■形式化方法包括: 规约( specification) o验证( verification) 形式验证包括: o定理证明( theorem proving 模型检验( model checking)形式化方法 ◼ 形式化方法是指为说明和验证复杂计算机系统所 采用的基于数学的语言、技术和工具。 ◼ 形式化方法包括：  规约（specification）  验证（verification） ◼ 形式验证包括：  定理证明（theorem proving）  模型检验（model checking）