文件名称：pgo：PGo是源代码，用于将PlusCal编译为Go lang
文件大小：5.59MB
文件格式：ZIP
更新时间：2024-02-21 07:33:41
go distributed-systems compiler tla pgo
围棋 PGo是编译器将规范编译为程序的源代码。 目的/动机 是用于指定/建模并发系统的语言。 它旨在编写。 特别是，PlusCal可以编译为TLA +，可以根据有用的系统属性（使用TLC模型检查器）进行检查。 例如，是有关互斥问题的PlusCal公式解决方案的资料库。 是Google为构建分布式系统而开发的一种基于C的语言。 它内置了对通道和goroutine并发的支持，这使其非常适合开发分布式系统。 当前没有工具将PlusCal / TLA +规范与规范的实现相对应。 PGo是一种工具，旨在通过基于PlusCal规范生成Go代码来将规范与实现联系起来。 PGo可以将经过验证的分布式系统算法的PlusCal规范转换为语义上等效的Go程序。 当前状态 积极开发中。 PGo支持将大多数单进程和非常简单的多进程PlusCal算法编译为相应的可编译且可运行的Go代码。 有关最新版本的手册快照，请参见资源库中的 ，其中详细介绍了已实现的功能和几个示例。 用法 要了解如何使用PGo，请参阅。 这个怎么运作 PGo是使用Java编写的源编译器。 它将在PlusCal扩展中编写的规范（称为Mo