一句话：提出定量最弱超前置演算，用谓词变换器统一正确性与不正确性超属性的推理。
现有最弱前置演算主要从单个初始状态出发推理程序终止后某量的期望值，无法直接刻画初始状态集合或初始概率分布上的定量超属性。本文提出一种面向非确定性与概率程序的定量最弱超前置演算：它以初始状态集合或初始概率分布为输入，为 hyper Hoare 逻辑提供最弱前置条件，并支持包括期望之外的方差等“超量”推理。作为副产品，还得到加权程序的最强后置条件演算，统一并扩展了现有最强后置与最强自由后置。该框架揭示了前向/后向变换器、正确性/不正确性以及非终止/不可达之间的新对偶关系。
We present a novel weakest pre calculus for reasoning about quantitative hyperproperties over nondeterministic and probabilistic programs . Whereas existing calculi allow reasoning about the expected value that a quantity assumes after program termination from a single initial state , we do so for initial sets of states or initial probability distributions . We thus (i) obtain a weakest pre calculus for hyper Hoare logic and (ii) enable reasoning about so-called hyperquantities which include expected values but also quantities (e.g. variance) out of scope of previous work. As a byproduct, we obtain a novel strongest post for weighted programs that extends both existing strongest and strongest liberal post calculi. Our framework reveals novel dualities between forward and backward transformers, correctness and incorrectness, as well as nontermination and unreachability.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ZhangZK024,
title = {Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers},
author = {Linpeng Zhang and Noam Zilberstein and Benjamin Lucien Kaminski and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689740}
}