时间: 2026-04-29 19:00-21:00 地点: 自强科技楼 5505 tunight pl
字符串和字符串操作在真实世界的编程任务中随处可见。主流编程语言的类型系统往往只用一种统一的String类型来表示任意字符串。为了更好的区分具有不同结构和语义的字符串（如 IPv4 v.s. IPv6 address），我们可以引入正则语言作为refinement type进行更加精确的分析和验证。其难点在于如何对正则语言和常见的字符串操作（如substring, contains, split）进行高效的推理。提起正则语言，人们往往会自然联想到自动机。但这种通用的、能登大雅之堂的理论方法复杂度较高。本次讲座将从Brzozowski derivatives的视角重新审视正则语言的推理问题，介绍一种不使用自动机，而完全通过操作正则表达式的抽象语法树的新方法。它可以用来验证Python的IPv6 address parser。
欢迎大家一起来玩！
活动信息：
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。