一、实验标题
初探软件工程形式化方法 + 《大象 ——Thinking in UML》读书总结
二、学习目的
系统理解形式化方法的定义、分类、技术特点与工程落地场景，区分形式化开发与传统自然语言开发的优缺点。
通过研读《大象 ——Thinking in UML》，掌握 UML 建模思想与面向对象分析设计逻辑，建立从需求到建模再到代码落地的完整思维链路。
对比 UML 半形式化建模与纯形式化方法的异同，理解软件工程不同开发范式的适用边界，夯实软件分析设计理论基础。
三、学习环境
资料环境：《大象 ——Thinking in UML》实体书籍、形式化方法学术文档、UML 建模工具（StarUML/ProcessOn）
软件环境：Windows 系统，在线 UML 绘图平台辅助案例画图练习
四、学习内容
（一）形式化方法知识梳理
- 基础定义
形式化方法是依托严格数学逻辑、集合论、自动机等数理基础，用标准化符号语言描述软件系统需求、约束与运行行为的软件工程技术，全程规避自然语言带来的语义歧义，可通过数学推导验证系统正确性。
通俗理解：把软件需求翻译成数学公式，用数学证明的方式校验程序是否符合设计规范。 - 两大分类
表格
分类 核心内容 特点
形式化规约 使用 Z 语言、VDM、Larch 等语言编写系统规格说明书，精准定义功能约束 偏需求描述，用于需求阶段精准落地
形式化验证 模型检测、定理证明，自动化校验代码 / 模型是否满足安全规范 偏测试校验，多用于高可靠项目 - 适用落地场景
多用于航空航天、轨道交通、军工嵌入式、金融核心系统等高安全等级项目，这类软件不允许运行故障；普通业务系统因开发成本高、学习门槛高较少全流程使用形式化开发。 - 优缺点总结
✅优点：需求无歧义、可数学证明正确性、从源头减少逻辑漏洞；
❌缺点：学习成本高、开发效率偏低、普通业务落地性价比差。
（二）《大象 ——Thinking in UML》读书总结
大象UML书籍封面
书籍第1版封面
- 书籍基础信息
本书由谭云杰撰写，是国内 UML 建模经典教程，豆瓣评分 8.1+，全书分为准备篇、基础篇、进阶篇、总结篇四大模块，摒弃枯燥语法堆砌，依托完整项目案例串联全流程建模知识。 - 全书核心内容拆解
准备篇：夯实面向对象基础（封装、继承、多态），纠正 “UML = 画图工具” 的误区，明确 UML 是面向对象分析的思考载体；
基础篇：详解 UML 五大类图（用例图、类图、时序图、活动图、组件图）的设计思想，说明每种图在需求、设计阶段的作用；
进阶篇：以一个真实业务项目为线索，从需求调研→用例梳理→领域建模→架构设计完整落地全流程 UML 建模，串联软件生命周期；
总结篇：答疑建模常见误区，区分 UML 半形式化与纯形式化方法的边界。 - UML 与形式化方法关联
UML 属于半形式化建模：部分语法规范、部分依赖自然语言补充说明；形式化方法是全数学符号描述，二者互补：普通项目用 UML 做工程建模，关键模块可叠加形式化验证提升可靠性。
五、学习心得体会
对形式化方法的感悟
之前开发习惯用自然语言梳理需求，很容易出现需求理解偏差；学习后意识到，高可靠性软件离不开形式化思想，即便日常项目不用全流程形式化开发，也可以借鉴其严谨思维规范需求文档，减少后期返工。
UML 读书收获
过去学习 UML 只死记各类图示画法，读完本书才理解：建模先思考业务，再画图表，UML 不是为了画图而画图，是把抽象业务具象化的工具；从 “写代码实现功能” 升级为 “先建模再编码” 的设计思维。
两种开发思想的互补思考
形式化偏重严谨数学证明、UML 偏重工程落地，实际开发中没有最优方案：互联网业务优先 UML 快速建模迭代，军工、车载等安全关键软件在 UML 基础上补充局部形式化验证。
六、学习总结
本次学习完成两大目标：吃透形式化方法的理论与应用边界、完整梳理《大象 ——Thinking in UML》全书核心知识点，厘清全形式化、半形式化（UML）两种软件工程建模路线。
知识落地规划：后续练习用 ProcessOn 完成小型项目全 UML 建模，尝试对项目核心模块用形式化规约思路撰写精简需求说明。
拓展方向：后续自学 Z 语言基础语法，尝试简单小程序的形式化规约编写，加深两种建模方式的实操理解。
