探索 AI 优先开发、编码护栏和可处置架构。
大语言模型在发现 test oracles 时是个不错的头脑风暴伙伴，但它们会产生幻觉性质，并遗漏领域约束。以下是如何在不发布虚假测试的前提下使用它们。
你需要测试一个函数，它的正确输出事先无法知道。路由优化器、情感分类器、物理模拟都可以。你读过 metamorphic testing：找到输入和输出之间必须成立的关系，然后测试这些关系而不是精确值。 问题在于如何想出这些关系。你盯着函数签名，脑子里一片空白。 于是你去问大语言模型。它在几秒内就抛出了十条…
并非所有 metamorphic relations 都能捕获 bug。弱关系给你虚假信心，强关系才能发现真正的缺陷。以下是如何区分两者，并构建一组真正有效的关系。
你为定价引擎写了十二条 metamorphic relations。每个测试都通过了，你对自己的覆盖率感觉良好。 然后有客户报告批量折扣算反了。你检查自己的关系套件，没有一个测试失败。你有加法一致性、单调性和幂等性的关系，却没有一个能捕获折扣乘数中的符号错误。 这是 metamorphic testing…
Metamorphic testing 让你无需知道确切的预期输出就能验证代码正确性。本文介绍它的工作原理、局限性以及如何开始使用。
你发布了一个为支持工单打标签的机器学习模型。测试套件全绿，每个测试都通过了。 但这些测试没有一个真正检查标签是否正确。你不知道正确答案是什么，也没人知道。对于真实世界的输入，"正确"输出实际上是不可知的，于是你只能退而求其次，检查函数没有崩溃，或者输出形状符合预期。这不是测试，这是碰运气。 这就是 oracle…
如何使用 phantom types 和 `this` 参数，将非法的协议转换从运行时 bug 变成编译期错误。
每个 API 客户端内部都藏着一个状态机。先握手，再认证，然后发送数据，最后关闭。打破这个顺序，你就会遇到运行时错误、服务器混乱，甚至更糟的静默数据损坏。 大多数团队用运行时检查来编码这些规则。。这确实有效——直到有人忘了写检查，或者一次 refactor 引入了一条跳过检查的新代码路径。等你发现时，bug…
OpenAPI 规范描述了请求和响应的 schema，但并未规定合法的消息序列。本文介绍你能从中提取什么，以及哪些地方仍需手动补全。
OpenAPI 规范告诉你合法的请求长什么样，合法的响应又长什么样。但它不会告诉你，在调用 之前能否调用 ；也不会告诉你，在调用 之后再调用 会发生什么。这些信息存在于 protocol spec 中，而 OpenAPI 并不是 protocol spec。 这就是缺口所在。你可以从 OpenAPI…
会话类型将通信协议编码到类型系统中，将运行时协议错误转化为编译时错误。以下是它们为何在论文中停留三十年才被生产代码采用的原因。
会话类型发明于1993年。三十年后，大多数网络服务仍然通过手写运行时检查来验证协议状态，如果它们验证的话。类型系统对于客户端是否在之前发送了，或者连接是否因为某人忘记关闭而泄漏，完全没有任何意见。…
会话类型将通信协议编码到你的类型系统中，在代码运行之前将消息传递不匹配转化为编译器错误。
死锁本应该是运行时问题。这就是它们如此烦人的原因。你的代码编译干净，测试通过，然后它在生产环境中卡住，因为进程A在等待进程B，而进程B在等待进程A。 会话类型扭转了这一点。它们将进程之间的通信协议编码到类型系统本身中。某些类别的死锁不再是运行时的意外，而开始成为编译器错误。你字面意义上无法编写会导致死锁的代码。…
如何使用Infer在CI管道中运行形式化静态分析，包含可工作的配置和现实权衡。
抽象诠释是那种会让工程师关掉标签页的术语。它听起来像是需要花一学期格论才能理解的东西。大多数开发者都以为它活在研究论文里，而不是在拉取请求中。…
大语言模型可以帮助分流静态分析中的误报，但它们无法像抽象解释那样理解程序语义。以下是如何将两者结合。
你的静态分析器刚刚在一个周五下午发出了847条警告。从统计上看，其中大约5%到15%是真正的缺陷。其余都是误报：生成代码中的无效存储、对工具来说可疑但对人类来说显而易见的空值检查、无关紧要的哈希函数中的整数溢出。 手动逐一排查令人心力交瘁。于是你想：能不能直接问LLM哪些是真的？…
Facebook如何利用抽象诠释和有意的不完整性，在数百万行Android代码中大规模发现竞态条件。
Facebook的Android应用有一个性能问题。UI线程被工作淹没，但将代码移到后台线程意味着竞态条件。投产崩溃。愤怒的用户。…