形式语义四大流派与规约语言三大类

形式化方法的实质是用逻辑、自动机、代数、图论等数学理论为基础，以一套特定符号和技术描述分析软件系统，价值在于提供精确无二义的描述手段、证明系统正确性或帮助定位错误的分析手段、以及支持开发过程自动化的方法工具。计算机语言的形式语义研究分四大流派，各自选择了完全不同的”意义寄托之处”。操作语义用抽象方法描述语言每个成分的执行效果——设计一个抽象机、定义抽象状态，指明抽象机每加工一个语言成分对状态的改变；与语言实现关系密切但难以用数学方法处理，对语义描述者所用的具体实现方法依赖很大。指称语义让语言每个成分对应一个数学对象（该成分的”指称”）——不涉及执行过程，只考虑各成分执行的最终效果，且认为最终效果不应依赖于执行过程本身。公理语义建立在程序正确性验证基础上，不做宏观全局的语义描述，而是给出一套逻辑系统（一组公理及推导规则），让人们能在给定前提下验证某个特定性质是否成立——它区别于经典逻辑的关键是把程序执行效果纳入了逻辑系统。代数语义把”描述语义的逻辑体系”和”满足这个逻辑体系的模型”区分开来，用代数方法处理满足同一逻辑系统的各种模型、把模型集合看作代数结构——它关心的不是单个模型，而是一整个”模型族”之间的关系。规约语言按对系统动态行为的刻画侧重点分三类：面向模型的规约（VDM、B、Z等）用集合序列映射等定义数据类型，操作靠前置条件和后置断言隐含定义；面向性质的规约（Larch、CASL等）不关心数据类型如何表示，只关心一个数据类型上各种操作的关系；面向进程的规约（CCS、CSP、π演算等）根据进程间交互来规约系统，重点是行为而非数据。面向进程的方法适合描述交互系统，面向模型和面向性质的方法适合描述转换系统——真实软件系统往往兼具交互和转换两面，所以不少形式化方法（如LOTOS结合ACT ONE、RAISE兼容三类）会混用多类规约方法。从行为和功能两个角度，还可以分出行为规约（刻画行为如何生成）和功能规约（描述行为间因果时序、输入输出转换关系，即行为本身是什么）这两个正交维度。