围棋 PGo是编译器将规范编译为程序的源代码。 目的/动机 是用于指定/建模并发系统的语言。 它旨在编写。 特别是,PlusCal可以编译为TLA +,可以根据有用的系统属性(使用TLC模型检查器)进行检查。 例如,是有关互斥问题的PlusCal公式解决方案的资料库。 是Google为构建分布式系统而开发的一种基于C的语言。 它内置了对通道和goroutine并发的支持,这使其非常适合开发分布式系统。 当前没有工具将PlusCal / TLA +规范与规范的实现相对应。 PGo是一种工具,旨在通过基于PlusCal规范生成Go代码来将规范与实现联系起来。 PGo可以将经过验证的分布式系统