形式化方法与大象thinking in uml 读书总结

一、什么是形式化方法

形式化方法是基于严格数学逻辑的软件开发、系统建模手段，用标准化符号、公式、逻辑证明替代自然语言描述，消除模糊歧义，分为三类：

1. 规格说明：用数学语言精准定义系统需求，避免文字漏洞；

2. 形式化验证：通过逻辑推导证明程序无死锁、无边界溢出、逻辑错误；

3. 形式化开发：从数学模型自动生成可执行代码。

适用场景：航空航天、芯片、金融支付、操作系统等高安全要求软件；普通业务系统很少使用，学习用来提升严谨思维。

二、《大象——Thinking in UML》读书笔记

1. 核心定位：UML统一建模语言实战书籍，不只是画图，教会面向对象分析与设计；

2. 核心内容：

◦ 用例图：梳理业务需求、用户场景；

◦ 类图：抽象实体、属性、关系（继承/组合/关联）；

◦ 时序图/活动图：梳理业务执行流程；

◦ 面向对象完整建模流程：需求→业务建模→系统建模→代码落地；