一、什么是形式化方法
以前我写代码，基本就是“需求看懂了，逻辑顺了，跑起来没bug就行”，从来没想过还有“用数学证明系统正确”这种操作…这次才知道，这就是形式化方法。简单说，形式化方法就是用数学和逻辑的“精准语言”，给软件写一份没有歧义的说明书，再用数学推理验证它的每一步行为都符合预期。
对比一下三种软件工程方法，一下就懂了：
• 非形式化方法：就是我们平时用的纯文字需求文档，优点是好写好懂，但缺点也致命——比如“用户快速登录”，到底1秒算快还是3秒算快？不同人理解完全不一样，后期很容易出问题。
• 半形式化方法：就是我们学的UML、数据流图这种，用图形化的方式建模，比文字严谨，又不会太复杂，现在大部分项目都是用这个。
• 形式化方法：完全基于数学逻辑，能证明系统的正确性，一般用在航空航天、医疗设备这种“出问题就出大事”的领域，门槛真的很高，对数学功底要求也很严。
以前总觉得“bug改改就行”，现在才明白，形式化方法的核心价值就是在写代码之前，就把设计里的漏洞、逻辑矛盾揪出来，从根源上减少返工。
二、读《大象——thinking in UML》阅读心得
老师推荐这本书的时候，我本来以为就是一本教“怎么画UML图”的工具书，结果读了几章，直接被打醒了！原来UML根本不是应付作业的“画图题”，而是一种面向对象的思维方式。它不是让你把需求翻译成一堆看不懂的图形，而是帮你从乱糟糟的业务需求里，一步步理清：
• 系统里有哪些角色（比如用户、管理员）
• 每个角色要做什么事（比如用户登录、管理员审核）
• 这些事之间怎么交互、有什么约束
就像书名里的“大象”，软件系统就像一头庞然大物，我们很容易只摸到局部，看不到全貌，而UML就是帮我们“摸清楚大象长什么样”的工具。以前学UML，我只会死记硬背用例图、类图、时序图的符号，完全没理解背后的逻辑。现在才明白，面向对象设计的核心不是“先写类，再写代码”，而是先搞懂业务，再把业务里的概念、关系抽象成模型。很多时候项目越写越乱，就是因为一开始没理清业务逻辑，只是用面向对象的语法写了面向过程的代码…
