Model execution allows us to prototype and analyse software engineering models by stepping through their possible behaviours, using techniques like animation and simulation. On the other hand, deductive verification allows us to construct formal proofs demonstrating satisfaction of certain critical properties in support of high-assurance software engineering. To ensure coherent results between execution and proof, we need unifying semantics and automation. In this paper, we mechanise Interaction Trees (ITrees) in Isabelle/HOL to produce an execution and verification framework. ITrees are coinductive structures that allow us to encode infinite labelled transition systems, yet they are inherently executable. We use ITrees to create verification tools for stateful imperative programs, concurrent programs with message passing in the form of the CSP and \Circus languages, and abstract system models in the style of the Z and B methods. We demonstrate how ITrees can account for diverse semantic presentations, such as structural operational semantics, a relational program model, and CSP's failures-divergences trace model. Finally, we demonstrate how ITrees can be executed using the Isabelle code generator to support the animation of models.

翻译：模型执行允许我们通过步进式探索可能行为（如动画与仿真）来对软件工程模型进行原型设计与分析。另一方面，演绎验证使我们能够构建形式化证明，以验证特定关键性质的满足性，从而支持高可信度软件工程。为确保执行与证明之间的结果一致性，我们需要统一的语义框架与自动化机制。本文在Isabelle/HOL中形式化实现了交互树（ITrees），构建了一个兼具执行与验证功能的框架。交互树是共归纳结构，能够编码无限标记转移系统，同时其本身具备可执行性。我们运用交互树为以下领域创建验证工具：带状态的命令式程序、采用CSP与\Circus语言形式的消息传递并发程序，以及遵循Z与B方法风格的抽象系统模型。我们展示了交互树如何兼容多种语义表示形式，包括结构操作语义、关系程序模型以及CSP的失效-发散迹模型。最后，我们演示了如何利用Isabelle代码生成器执行交互树，从而支持模型动画化验证。