结构正确性:构建可验证系统的关键原则

比特币

在软件开发中,类型系统因其能在编译时捕获大量错误而广受赞誉。类型系统通过将程序描述为类型、函数、特征等节点以及它们之间的关系(如返回、接受、实现等边)的图结构,为开发提供了明确的语法和词汇。这种图结构化的描述不仅限于类型系统,现代工具如构建系统、接口描述语言和数据库也广泛采用类似的方法来验证系统的正确性。 构建系统如Bazel将构建目标视为节点,依赖关系作为边,确保系统的封闭性和可部署性。接口描述语言则通过消息类型和服务节点以及参数和返回类型边来定义接口。数据库通过外键和约束条件来描述表之间的关系,但也依赖非结构性的约束条件来补充描述无法通过结构性描述的有效性。

结构正确性的核心在于将领域模型化为类型化的节点和边的图结构。最优秀的图结构系统具有定义性,即描述系统的结构即是系统本身。例如,Bazel中的构建目标无法访问未声明的依赖,这不仅确保了系统的可验证性,也简化了系统的描述。这种定义性图结构化系统能够同时定义系统的有效性和输出的计算方式,使得开发者在描述系统结构的同时,也获得了验证系统的能力。 不同领域的图结构化系统各有其独特的节点和边类型。Bazel通过不同的边类型(如deps、srcs、data)定义不同的能力,使得工具既表达丰富又易于理解。

这种结构化的描述不仅限于构建系统,还可以扩展到服务、数据集等多个领域。例如,服务、其指标端点和Prometheus部署可以作为同一图结构中的节点,其关系一经声明,即可用于编译、部署和验证整个系统。 然而,结构正确性在处理状态时面临挑战。数据库通过模式指定表和外键来定义可存储的数据,但状态转换的有效性通常由应用层实现,这往往导致错误。例如,两个端点可能同时修改订单状态,其中一个端点可能忘记检查库存。 彩色Petri网(CPN)通过严格定义状态转换来解决这一问题。

CPN中的状态仅通过特定的绑定和转换来变化,消耗、变异和生产特定位置的标记。这种图结构化的状态管理使得系统的正确性可以通过图结构本身来验证。例如,在一个网络爬虫的例子中,CPN通过单一转换(select_resource)原子化地租用代理、增加域的活动计数和创建会话,无需担心锁策略的正确性。代理保存的性质是网络的拓扑事实,即代理标记在任何时间点只能存在于可用代理或租用代理中,且仅声明的转换可以移动它。 CPN将状态和转换统一,使得系统的正确性可以通过图结构本身来验证,而无需依赖分散的应用代码、单元测试和数据库约束。这种统一性不仅提高了系统的可靠性,也简化了开发过程。

尽管CPN作为新兴领域,仍有许多关于潜在错误和性能权衡的问题需要探索,但其潜力巨大,值得深入研究。 。