Dafny中正则表达式的良好（Co）代数语义

正则表达式通常以其谓词语义来理解，即通过形式语言——正则语言。这种观点的本质是归纳的：两个基本元素若以相同方式构造，则等价。或者，正则表达式可通过其操作语义来理解，即通过确定性有限自动机。这种观点的本质是共归纳的：两个基本元素若在分解方式相同，则等价。据克莱恩的著名定理所知，两种观点是等价的：正则语言恰好是由确定性有限自动机接受的形式语言。在本文中，我们使用Dafny这一一种验证感编程语言，首次形式化地验证了——即在此之前仅通过手工证明所建立的——两种正则表达式语义在良好意义上是相同的，即它们在点到点的双相似性（pointwise bisimilarity）下是等价的。在我们的形式化过程中，每一步都提出了一种Coalgebra语言中的解释。我们发现Dafny特别适合此任务，因为其归纳和共归纳特性，希望我们的做法为未来对其他理论的泛化提供了蓝图。