反应式设计契约的统一理论

契约式设计是一种重要的基于模型的设计技术，其中复合系统由一组契约来规约，这些契约规定了每个组件的行为假设与保证。在本文中，我们描述了一种用于反应式设计契约的统一理论，为反应式系统的建模与验证提供了基础。我们提供了一种用于契约表达与组合的语言，并辅以丰富的演算理论支持。与文献中的其他语义模型不同，我们的契约理论允许我们同时规约状态变量的演化以及与环境的允许交互。此外，我们的交互模型是抽象的，并支持例如离散时间、连续时间和混合计算模型。基于统一编程理论（UTP），我们的理论可进一步与计算理论组合，以支持多范式语言的语义。我们通过证明框架Isabelle/UTP提供了实用的推理支持，包括一个证明策略，该策略将关于反应式程序的猜想归约为三个谓词，以符号方式刻画其关于中间与最终观察的假设与保证。这使我们能够验证具有大型或无限状态空间的程序。我们的工作推进了反应式语言语义、其契约规约描述以及组合验证方面的技术前沿。