形式化规格说明语言的两大流派与代表语言

形式化规格说明语言的研究分两大流派，划分标准是”用什么数学工具描述系统”：基于模型的方法用已知特性的数学抽象为目标系统的状态和行为特征直接构造模型，代表语言有Z语言、B语言、VDM、Petri网——每种方法各提出一套自己的规范体系，但规范所用的数学工具本身并不能自动保证规范是正确的，即使借助证明技术辅助确认，也只能缩短形式化方法与现实世界的距离、无法彻底消除差距。代数方法则不直接建模系统状态，而是为规格说明提供描述抽象概念、进程间连接与推理的特殊机制，代表语言有CSP、CCS、CLEAR——对开发人员要求更高、描述往往难以理解（”只能为’小众’服务”），且可扩展性差，架构一旦修改就要重新做代数计算和验证，代价很大。四种基于模型的语言各自的差异化定位是：Z语言用”模式=声明+谓词”的方式表达系统状态和操作，应用最广泛、通用性最强；Petri网用库所/变迁/有向弧/令牌四元组描述并发系统，尤其适合刻画软件架构的动态演化性（如组件增删改后的波及效应分析）；B语言用抽象机符号（AMN）支持从规格说明到实现的分层构造，适合大型软件开发中降低复杂性；VDM用一阶谓词逻辑和抽象数据类型描述运算功能，强调”先抽象后具体”的自顶向下开发思想、并为程序正确性证明提供依据。选择哪种语言本质上是在”通用性”“并发/动态建模能力”“到实现的可追溯性”“正确性证明能力”这四个目标之间做取舍，没有一种语言能同时最优。