形式化并不是一个读完定义就算掌握的知识点，更像一组需要逐渐养成的阅读习惯：认出论文正在讨论的对象，跟上规则推动状态变化的过程，再判断分析结果究竟做出了怎样的保证。面对一整套新概念时，真正困难的往往不是某一页，而是不知道应该先读什么、后读什么。 这张阅读地图因此不急着讲具体公式，而是帮你安排路线。前六篇构成一条从“读懂符号”到“判断分析方法”的主线：前半程建立程序状态、语义与抽象的直觉，...

今天，我们已经习惯让程序处理银行交易、控制汽车、分配云端资源，甚至生成新的程序。但如果把时间拨回计算机尚未诞生的年代，一个更根本的问题仍悬而未决：所谓“按照步骤完成计算”，究竟是什么意思？哪些问题可以交给机器，哪些问题无论给它多少时间也无法解决？ 这个好奇心后来引出了一条意想不到的历史线索。数学家先用纸笔想象机器，程序员随后发明语言命令真实的机器；当程序越来越长，人们又不得不追问一句代...

一个代码模型收到 bug 报告，很快给出补丁。代码能够编译，现有测试也全部通过，reviewer 看了一眼，觉得改法十分自然。两周后，一个测试集中没有覆盖的输入再次触发故障：补丁只是绕过了样例，并没有修复真正的错误。 这个故事并不说明大模型不会写代码。恰恰相反，它说明生成一段“看起来正确”的程序已经很容易，而判断它对所有相关输入是否满足要求仍然很难。模型可以提出候选实现、测试、断言甚至证明...

凌晨两点，一个静态分析任务还在 CI 服务器上运行。它确实比旧版本精确：区分了更多调用上下文，也追踪了更多路径；可开发者已经等了四十分钟，最后选择跳过检查。另一套工具只用两分钟，却一次报告了几百条警告，其中大部分并不会发生，同样没人愿意逐条处理。 这两个失败指向同一个事实：理论上正确的分析，还不一定是工程上可用的分析。真实工具必须同时考虑是否漏掉行为、结果是否足够精确、算法能否终止，以及它...

想象一名分析器沿着控制流图巡查程序。走过赋值语句，它更新变量信息；来到分支，它复制状态分别前进；遇到汇合点，它把两条路径的发现合在一起。最麻烦的是循环：新的信息会沿回边送回旧节点，迫使分析器重新检查已经看过的代码。 如果这种巡查没有明确规则，分析器要么漏掉路径，要么永远绕着循环打转。真正让它运转起来的，是三个彼此衔接的部件：transfer function 负责处理一条指令，join 负...

假设我们想检查一个来自用户输入的整数是否可能越界。最直接的办法，是记录它在每条执行路径上的确切取值；可惜输入可能有无穷多种，循环还会不断产生新状态。分析器如果坚持“一个值也不丢”，很快就会被这些细节淹没。 x = input(); if (x > 100) { ... } 真正有用的问题往往不是“x 到底等于多少”，而是“它是否为正”“是否可能为空”或“是否来自不可信输...

人读程序时，很容易顺着代码从上往下看；分析器却不能只走眼前这一条路。一次条件判断会产生分支，一个循环会把执行带回原处，异常和返回语句还可能让程序提前离开。 要分析程序，首先得把所有可能的去向画出来，再说明每走一步，程序状态会发生什么变化。这篇文章就从这两个问题出发：程序能走到哪里，以及到达那里时状态变成了什么。 上一篇文章已经把程序状态理解为“变量到值”的映射： [\sigma:X\r...

一位刚进入课题组的硕士生第一次参加论文讨论时，在方法章节旁边写满了问号。他认得“变量”“状态”和“赋值”这些词，却说不清作者为什么要换一套符号重新描述它们。更让人沮丧的是，每个符号单独看都不陌生，连在一起却像一句无法断句的话。 讨论开始后，导师没有让他先去补高等数学，而是指着定义问了三个朴素的问题：这里定义了什么对象？对象之间是什么关系？这条规则让程序状态发生了什么变化？当公式被按这个顺序...

本文记录如何在 VMware Fusion 中，让 Ubuntu 虚拟机通过 Mac 上的 VPN/代理软件访问 Google、GitHub、apt 源等外网资源。 实验环境示例： 宿主机：macOS 虚拟机软件：VMware Fusion 虚拟机系统：Ubuntu Server VMware 网络模式：Share with my Mac Mac 代理软件：Flyi...

As the last article of this series, today we will discuss the denotational semantics for imperative programs. Specifically, we will check out how to apply CPO model on the $\text{while}$ programs i...