验证图程序的单体二阶逻辑性质

在 Hoare 风格或 Dijkstra 风格的图程序证明系统中，核心挑战在于针对规则和后置条件定义最弱 Liberal 前置条件（weakest liberal precondition）构造。此前解决该问题的工作主要关注针对一阶性质的断言语言，这类语言无法表达图的重要全局性质，如无环性、连通性或路径存在性。本文扩展了 Habel、Pennemann 和 Rensink 提出的嵌套图条件，使其表达能力等价于图上的单体二阶逻辑（monadic second-order logic）。我们针对这些断言提出了最弱 Liberal 前置条件构造，并演示了其在验证 Habel 等人意义上的图程序非局部正确性规范中的应用。