基于反应关系与 Kleene 代数的反应式程序演算验证

反应式程序在现代应用中无处不在,因此验证极为重要。我们提出一种针对具有大或无限状态空间的反应式程序的验证策略,利用反应关系的代数定律。我们定义了新的算子来刻画交互与状态更新,以及相关的等式理论。借此我们可以计算反应式程序的指称语义,从而促进自动化证明。值得注意的是我们对带有反应式不变量的迭代程序的推理支持,其由 Kleene 代数支撑。我们通过验证一个反应式缓冲器来说明我们的策略。我们的定律与策略在 Isabelle/UTP 中形式化,这提供了可靠性保证与实用的验证支持。