一、背景
核心目标是让我们跳出 “写代码” 的思维，理解软件工程中建模与验证的核心思想。两个任务看似独立，其实底层逻辑是相通的 —— 无论是形式化方法还是 UML 建模，本质都是用严谨的方式描述系统，消除歧义，保证系统的正确性。
二、什么是形式化方法？—— 从 “写代码” 到 “证明代码”
2.1 通俗理解：形式化方法到底是什么？
简单来说，形式化方法就是用数学、逻辑的方式来描述和验证系统，把我们平时写的 “模糊的需求”，变成 “严谨的数学模型”，再通过数学推理证明系统的关键性质是成立的，而不是靠 “写代码 + 反复测试” 来碰运气找 bug。
举个很直观的例子：
非形式化的做法：写一个银行转账系统，写完代码后，手动测几百次转账场景，看看有没有余额错误、负数余额的 bug；
形式化的做法：先给系统建立数学模型，用谓词逻辑定义 “转账前后的余额关系”，再通过模型检查证明 “无论转账多少次，余额都不会出现负数、不会凭空消失” 这些性质，从根源上保证系统不会出这类问题。
2.2 形式化方法的核心思想
形式化方法的核心可以拆成三个关键点：
形式化描述：用严格的语法和语义定义系统，比如用有限状态机、Petri 网、一阶谓词逻辑等工具，描述系统的状态、行为和约束，没有任何歧义；
形式化验证：通过数学推理、模型检查、定理证明等方法，验证系统是否满足需求中定义的关键性质（比如安全性、一致性、无死锁）；
事前保证正确性：它的目标不是 “找 bug”，而是 “证明系统没有这类 bug”，从 “事后测试兜底” 变成 “事前保证正确”。
2.3 形式化方法 vs 非形式化方法
很多人会疑惑：既然形式化方法这么好，为什么平时写业务代码很少用？我们可以用一个表格对比两者的差异：
对比维度 形式化方法 非形式化方法（自然语言 / 流程图 / 测试）
描述方式 数学 / 逻辑符号，严格无歧义 自然语言 / 图形，可能存在歧义、理解偏差
验证方式 数学证明、模型检查，可验证所有场景 测试、人工评审，只能覆盖部分场景
适用场景 高安全、高可靠系统（航空航天、铁路信号、金融核心） 普通业务系统、快速迭代项目
成本 高，需要专业工具和人才，学习曲线陡峭 低，上手快，适合大多数场景
2.4 形式化方法的应用与局限
形式化方法不是 “万能药”，它有明确的适用边界：
应用场景：航空航天的飞控系统、铁路信号控制系统、金融核心交易系统、操作系统内核（比如知名的seL4微内核，就是通过形式化验证证明了其功能正确性）；
局限：对于复杂的业务系统，建模成本极高，而且无法覆盖所有非功能需求（比如用户体验、性能），普通互联网项目很少会用到。
三、《大象 ——Thinking in UML》阅读心得：建模不是画图，是讲清楚故事
老师推荐的《大象 ——Thinking in UML》，我之前以为是一本教你 “怎么画 UML 图” 的工具书，读完才发现，它根本不是一本 “画图教程”，而是一本讲面向对象分析与设计（OOAD）思想的书，UML 只是一个载体，核心是教我们 “如何用模型理解和描述系统”。
3.1 这本书到底在讲什么？
很多新手学 UML，会陷入一个误区：把 UML 当成画图工具，背熟了类图、时序图、用例图的画法，却不知道画这些图是为了什么。
而《大象》这本书，从 “需求” 出发，一步步教我们：如何从用户的视角理解系统，如何把业务需求转化为用例模型，再到分析模型、设计模型，最后落地到代码。它的核心不是 “怎么画”，而是 “为什么画”——UML 是一种半形式化的建模语言，本质是团队沟通的 “通用语言”，用来消除需求方、产品、开发之间的理解偏差。
3.2 我的几个核心收获
读完这本书，我对 “建模” 这件事有了完全不一样的理解：
UML 是沟通的语言，不是炫技的工具
之前我以为画 UML 图是给别人看的，是 “软工课的作业”，现在才明白，UML 的本质是消除歧义。比如一个 “用户下单” 的场景，用自然语言描述，十个人可能有十种理解，但用 UML 时序图画出来，谁调用谁、谁和谁交互，一眼就能看明白，这和形式化方法 “消除歧义” 的目标是完全一致的，只是 UML 更偏向业务建模，形式化方法更偏向数学验证。
建模的第一步，是站在用户的视角看系统
书里反复强调 “用例驱动”，建模不是上来就画类图、想怎么写代码，而是先搞清楚：系统的用户是谁？用户需要系统帮他做什么？比如我们做的芋头病害识别系统，先想清楚 “用户上传图片、系统返回识别结果” 这个核心流程，再去设计对象和交互，而不是上来就写Image类、Model类。
模型是演进的，不是一次成型的
很多人以为模型是 “一次性画好，之后照着写代码就行”，但书里说，模型是从高层到低层逐步细化的：需求阶段的用例模型、分析阶段的交互模型、设计阶段的类模型，每一步都是对上一层模型的细化，和形式化方法的 “从抽象模型到实现模型” 的过程是相通的。
面向对象的本质，是思维方式，不是语法糖
书里讲，封装、继承、多态不是 Java 的语法糖，而是面向对象的思维方式：把现实世界的事物抽象成对象，把复杂的问题拆分成一个个独立的对象，降低系统的复杂度。建模的本质，就是通过抽象和简化，把复杂的系统变得可理解、可维护。
3.3 形式化方法和 UML 建模的联系
这两个作业点，其实底层逻辑是完全相通的：
UML 是半形式化的建模语言，有严格的语法规则，但语义没有形式化方法那么严谨，适合业务系统的建模和团队沟通；
形式化方法是完全形式化的，有严格的语法和语义，适合关键系统的正确性验证；
两者的核心目标，都是 “用模型描述系统，消除歧义，保证系统的正确性”，只是适用的场景和严谨程度不同。
四、小结：建模思维，从入门到上路
这次作业让我跳出了 “只会写代码” 的舒适区，第一次真正理解了软件工程中 “建模与验证” 的价值：
形式化方法让我明白，“保证系统正确” 不只有 “测试” 这一条路，严谨的数学建模和验证，是高可靠系统的基础；
《大象》这本书让我明白，建模不是为了应付作业，而是为了更好地理解系统、沟通需求，避免写一堆 “自己都看不懂” 的代码。
对于我们学生来说，不用一开始就啃形式化方法的硬核理论，先学会用 UML 建模，培养建模思维，理解 “模型是用来解决什么问题的”，再去接触更严谨的形式化方法，是一个很好的成长路径。