理解“形式化方法”是迈向高阶软件工程思维的关键一步。这不仅仅是学习一种技术更是从“实现功能”向“保证正确性”的思维转变。1. 什么是形式化方法简单来说形式化方法是基于数学的软件开发技术。在传统的面向对象编程中我们通常用自然语言中文或英文写需求文档用UML画图。但自然语言往往有歧义UML图有时也不够精确。形式化方法使用形式化规约语言基于数学逻辑来精确描述系统的行为。它主要包括两个核心部分形式规约用数学公式定义系统“应该做什么”。形式验证用数学推导证明系统“做得对不对”。2. 为什么要引入形式化方法在面向对象设计中引入形式化方法主要为了解决以下问题消除二义性数学语言是精确的。例如规定age 0计算机就能严格判断不会有“年龄应该是正数吧”这种模糊理解。早期发现错误在写代码之前通过检查规约就能发现逻辑漏洞比如死锁、状态不可达。契约式设计这是面向对象中最重要的应用。它强制要求代码实现必须满足预先定义的“契约”前置条件、后置条件、不变式。3. 核心概念契约式设计它将程序看作一系列“契约”的集合。你需要掌握以下三个关键词表格关键词含义作用前置条件方法执行前必须满足的条件调用者的责任例如传入参数不能为null后置条件方法执行后必须保证的结果被调用者的责任例如返回列表不为空且包含新元素类不变式对象在其生命周期内始终保持为真的属性保证对象状态的一致性例如人的年龄永远不能小于04. 常见的形式化工具与语言通常会涉及以下两种具体的形式化描述方式A. JMLJML 是一种专门用于 Java 的规格语言它以注释的形式写在代码中。B. UML 与 OCL虽然 UML 类图是图形化的但为了使其精确通常会配合OCL使用。OCL 是一种形式化语言用于在 UML 模型上添加约束。例子在 UML 类图中你可以用 OCL 表达“一个订单必须至少包含一个商品”这样的约束这是单纯画图无法表达的。