写Java的都知道并发编程是噩梦。你写了一个ConcurrentHashMap的缓存逻辑JUnit测了100遍都通过上线后第101次请求还是可能死锁。为什么因为测试只能证明存在bug不能证明没有bug。在Java多线程的混沌世界里线程调度、内存可见性、指令重排序的组合是天文数字人脑根本穷举不完。形式化方法Formal Methods 做的就是这件事用数学在代码运行之前证明系统在所有可能状态下都不会出错。它分两步规约Specification用数学语言精确描述系统应该做什么验证Verification用逻辑推理或模型检测证明系统确实做到了1.2 工业界已经在用的轻量级工具很多人一听形式化就想到满屏希腊字母。其实现在有很多轻量级工具已经在用了工具 用途 使用者TLA 验证并发/分布式算法 Amazon AWSAlloy 快速原型验证 学术界Z3 约束求解 微软对Java学生来说最值得关注的是 TLA。它专门对付并发和分布式系统的逻辑错误——这正是Java后端最头疼的领域。1.3 一个让我起鸡皮疙瘩的例子TLA 是图灵奖得主 Leslie Lamport 发明的。我用它写了一个24小时时钟VARIABLE clockInit clock ∈ 0…23Next clock’ IF clock 23 THEN 0 ELSE clock 1TypeInvariant clock ∈ 0…23如果你手滑写成 clock’ clock 1忘了23归零TLC 模型检查器会立刻甩给你一个反例State: clock 24我不需要想到所有边界情况机器会帮我把所有状态空间遍历一遍。 这就是形式化方法的魅力——把人脑穷举变成机器自动证明。想象一下如果你在写Java的分布式锁、订单状态机、或者线程池调度逻辑时能在编码前就用数学证明没有死锁、没有竞态条件那还要什么synchronized的盲目试错二、《大象——Thinking in UML》你的类图可能画错了2.1 书名已经告诉你答案谭云杰用大象比喻软件系统盲人摸象系统太复杂每个人都只能看到局部大象无形UML不该是僵化的绘图规范而应是一种内化于心的建模思维2.2 一句话颠覆认知UML的单词是元素语法是建模方法。以前我觉得UML就是画几张类图给答辩老师看。现在才明白当你能用用例图、类图、时序图清晰表达系统里有什么对象、它们如何交互你就掌握了Java面向对象的本质。2.3 两个真正重要的概念边界Boundary决定系统的里和外。边界不清耦合必高。抽象层次控制复杂性的唯一手段。自顶向下逐层细化像剥洋葱。不要在一个Controller里既谈业务规则又谈数据库字段。2.4 面向对象不是把所有代码包成class书里把大象装进冰箱的例子很经典面向过程打开冰箱门 → 装大象 → 关门关注步骤面向对象冰箱.开门() → 冰箱.装进(大象) → 冰箱.关门()关注对象职责Java的面向对象不是写一堆public class再强行套个Spring注解而是把现实世界的行为分配给合适的对象。 你写的每一个Service和Entity到底是在分配职责还是在堆砌函数三、硬币的两面架构师的两只眼睛查完资料突然顿悟形式化方法和UML是互补的。UML / 《大象》 形式化方法目标 看见全貌、建立共识 证明正确、消除歧义手段 可视化建模、抽象分层 数学规约、逻辑验证解决 “做什么和谁来做” “做得对不对”思维 感性、宏观 理性、微观UML让我们看见大象形式化方法让我们算清大象的每一步。对一个Java后端来说理想的工程流程应该是先用UML对齐需求和架构用例图、领域模型、时序图再对核心模块——比如分布式事务、状态机、并发控制——用形式化方法上保险最后用Spring Boot把设计落地成代码四、结语不止于CRUD以前我觉得Java后端就是Spring Boot MyBatis Redis 写CRUD。但是软件工程一直在回答同一个问题人类如何驾驭复杂性UML的答案是抽象、边界、可视化让我们的大脑能处理超载的信息形式化方法的答案是数学严谨性让机器验证人脑无法穷举的逻辑谭云杰说UML应大象无形Lamport 说不用形式化思考就没有真正理解系统。
