什么是形式化⽅法？
PS：软件⼯程作业，⽼师要求⾃⼰去阅读和了解形式化⽅法是什么，⾃⼰查阅了⼀下，感觉实在是难懂......
正⽂：
1 形式化⽅法基本概念
形式化⽅法是基于严格数学基础, 对计算机软(硬)件系统进⾏形式规约、开发和验证的技术.其中, 形式规约使⽤形式语⾔构建所开发的软件系统的规约, 它们对应于软件⽣命周期不同阶段的制品, 刻画系统不同抽象层次的模型和性质, 例如需求模型、设计模型甚⾄代码和代码的执⾏模型等.形式验证是证明不同形式规约之间的逻辑关系, 这些逻辑关系反映了在软件开发不同阶段软件制品之间的需要满⾜的各类正确性需求.例如, 形式验证给出“系统设计模型满⾜若⼲特定性质”的证明构造.在形式规约和验证的基础上, 形式化开发主要是构造、证明形式规约之间的等价转换和精化关系, 以系统的形式模型为指导, 逐步精化, 开发出满⾜需要的系统, 也称为构造即正确(correct by construction)的开发. 形式化⽅法与其他软件开发⽅法[]的主要区别在于：其描述软件及其性质的语⾔是⽆歧义的, 构造和验证
软件的⽅法是严格的.在软件⼯程中,
形式化⽅法提供了⼯程化系统设计的⼀种⽐较透彻的思维⽅式, 可以很好地⽀持抽象模型建⽴、系统精化、模型和证明重⽤; 形式化开发过程具有很好的可重复性, 相应的软件制品模型也具有较强的可分析性和可验证性.因⽽, 形式化⽅法可以有效地提⾼和保障系统的可信性.
形式化⽅法与计算机科学理论密切相关, 其发展与程序设计语⾔和程序理论的发展息息相连.作为⼀个学科⽅向, 它研究形式化⽅法的数学基础、形式系统的表达能⼒、形式系统的推理系统及其可靠性和完备性, 以及在计算系统开发和⽣命周期各个阶段的理论、⽅法、技术、⼯具和应⽤⽅式等. 1.1 历史回顾
形式化⽅法的发展已有较长的历史, ⼈们主要从两个⾓度出发推动形式化⽅法的提出和早期发展, 即, 为程序设计提供数学基础的理论研究⾓度以及为软件开发提供严格质量保证的软件⼯程⾓度.早在1949年, Turing的论⽂“Checking a large routine”即讨论了程序的正确性问题[].1962年, McCarthy在IFIP上做了题为“通往计算的数学科学”的演讲[], 系统论述了程序语⾔的形式语义和程序设计理论重要性, 直接触发了形式语义研究. 1968年在德国Garmisch召开的NATO软件⼯程会议, 从提⾼软件质量和⽣产率的软件⼯程⾓度出发, 提出了要建⽴软件开发和⽣产的数学基础; 进⼀步地, 软件的正确性问题和概念成为1969年NATO软件⼯程会议的主题之⼀.形式化⽅法在这种历史背景下成为程序设计和软件⼯程基础 威特金大学的重要组成部分, 先后出现了⼀批有重要影响的⼯作.给出了部分图灵奖获奖者在形式化⽅法⽅⾯的研究⼯作.
Table 1 Examples of formal methods researches by Turing Award Laureates表 1 部分图灵奖获得者在形式化⽅法⽅⾯的研
究
1.1.1 围绕形式语⾔和形式语义学的基础研究(1930年~⾄今)
形式语⾔是由符号化字母表以及递归的语法规则完全定义和⽣成所有表达式或语句的语⾔.形式逻辑的语⾔都是形式语⾔, 如命题逻辑、谓词逻辑和布尔代数.20世纪30年代, Church⽤形式语⾔定义研究计算和算法, 提出了⼀种计算模型Lambda演算[, ], 后来成为函数式程序设计语⾔、类型论和操作语义的理论基础.事实上, Lambda演算本⾝可以看作是⼀种程序语⾔.在20世纪50年代末, ⾼级程序设计语⾔的定义开始了关于计算的形式系统的研究, 产⽣了Backus-Naur Forms(BNF范式)并⽤于定义ALGOL60, 形成了语⾔的递归抽象.形式语⾔不仅在语⾔的定义中得到了应⽤, 在系统软件开发中也发挥了作⽤, 例
如, UNIX中的yacc和grep的开发[].在形式语⾔定义的同时, 如何定义程序的含义成为关注的焦点[], 形式语义学的研究逐渐形成了四⼤体系：操作语义、指称语义、代数语义和公理语义.在定义ALGOL68的语义时, ⾸次使⽤了“操作语义”这个术语, ⽽McCarthy已在1960年⽤Lambda演算定义了LISP的语义[].形式语⾔理论和形式语义学为形式化⽅法奠定了基础, 不仅⽤来定义程序设计语⾔, 形式系统还⽤来严格定义规约语⾔的基础, 建⽴了形式规约语⾔或形式化建模语⾔.20世纪60年代, Petri提出了Petri Net作为分布式系统的数学化建模语⾔[].⾯向并发系统, Hoare提出了通信顺序进程CSP[, ], Milner提出了通信系统演算CCS[, ], Hennessy和Lin提出了消息传送进程的符号互模拟理论[].随着软件形态的不断变化, 形式化建模语⾔也不断发展.例如, 针对反应式系统, Pnueli在1977年引⼊了线性时序逻辑LTL[], Clarke和Emerson在1981年建⽴了计算树逻辑CTL[]; 在反应式系统描述的基础上, 发展了⾯向实时系统的TPTL[]、Timed Automata[]、Timed Regular Expressions[]和Timed CSP[]以及Timed CCS[], 还出现了硬件描述语⾔、体系结构描述语⾔、通信控制建模仿真语⾔等.
1.1.2 围绕形式规约和开发的⽅法学研究(1970年~⾄今)
直接使⽤程序设计语⾔及其语义难以描述和证明软件从需求⽂档到程序代码的开发过程各阶段创建的不同抽象层次的制品及其正确性, ⼈们开始研究⾼层抽象的形式规约语⾔的设计, 形成了以形式规约语⾔为基础的形式化开发⽅法.例如VDM[-]、Z[]、Event-B[]、RAISE[, ]、CafeOBJ[]、TLA+[]、rCOS[]、SOFL[]等等.形式化开发利⽤形式规约语⾔对软件建模并描述其所期望的软件性质, 提供指导开发⼈员
进⾏精化的⽅法, 进⾏形式规约之间(部分的)⼀致性检查和证明.基于不同的开发⽅法, 形式规约可以⾃顶向下逐步精化形成开发的规约序列, 在⾜够的实现细节完成后, 可以通过代码⾃动⽣成得到程序.例如, VDM的精化有数据具体化(data reification)和操作分解(operation decomposition)等.形式化⽅法逐步建⽴了⼯具集, 以⽀持形式规约的性质分析和证明, 例如Z/EVES[]、Event-B/Rodin[].1970年代后, 软件⼯程界认识到了数学可以为保证程序正确性提供技术基础, 形式化⽅法(formal methods)⼀词开始传播开来.1980代初, 唐稚松提出以时序逻辑作为软件开发过程的统⼀基础, 并着⼿建⽴XYZ系统[].在1980年代到90年代, 形式化⽅法得到了重视, 特别是欧盟⼤⼒⽀持了形式化开发⽅法的研究.例如Concur、ProCoS、REACT等.⼈们希望能够利⽤形式化⽅法⾼效、⾼质量地开发软件, 这⼀⽅⾯有⼒地促进了形式化⽅法和技术的发展; 另⼀⽅⾯, 由于应⽤规模较⼩, 效果证据不⾜, 应⽤⽅式不明确, ⼯业界对形式化⽅法的看法出现了争议.在形式规约和开发的⽅法学基础⽅⾯, Goguen和Burstall提出了机构(institution)的抽象模型理论, ⽤以建⽴语⾔语法驱动的、不同形式逻辑基础上的各种形式化⽅法的理论统⼀以及技术和⼯具集成与和谐使⽤[]; Hoare和何积丰提出了统⼀程序设计理论框架UTP, 提供了在⼀种程序(如顺序程序)语义模型理论基础上构建扩展程序(如并发)的语义理论, 从⽽保证原来的理论在扩展的理论中重⽤, 并同时建⽴了操作语义、指称语义、公理语义和代数语义的互联统⼀[].
1.1.3 围绕形式验证技术的⼯程化研究(1980年~⾄今)
建⽴了形式规约之后, 如何从形式规约开发得到正确的系统成为关键.形式验证, 包括如何证明不同抽象
层次的规约间等价或者满⾜精化关系、如何验证形式规约(所要求的性质)及其模型之间的满⾜关系, 是形式化⽅法保证软件开发正确性必须解决的科学问题和实际应⽤问题.形式验证理论涉及了数理逻辑的传统基础问题.在研究验证⾃动化过程中, 发现了相关⼤量的不可判定问题、NP完全问题以及状态爆炸等否定性的结果.否定性的结果同时推动了各种可组合的规约证明技术、抽象解释技术以及提⾼实现效率的数据结构(如BDD).这些研究同时促进了形式化技术与传统测试和仿真技术的结合, 形成了新的基于形式化的测试和仿真技术.这些技术将重点放在软件的缺陷检验和调试上, 以发现错误为⾸要⽬的[], 出现了形式验证及其⼯程化技术和⼯具, 包括以SAT/SMT为代表的约束求解、基于交互式辅助定理证明⼯具的机械化验证、以模型检验为代表的⾃动分析与验证.⼯具的⾃动化⽔平和可扩展能⼒得到了显著的提⾼, 如SAT/SMT求解器Chaff[]、Z3[]、CVC4[]，定理证明环境ACL2[]、Isabelle/HOL[]、Coq[]和PVS[], 模型检验⼯具SMV[]、SPIN[]、UPPAAL[], PRISM[]、PAT[]等等.形式验证在硬件验证中获得了巨⼤的成功, 也不断地进⼊嵌⼊式软件、安全攸关软件等⾼安全等级软件的开发.Pnueli在他的图灵奖演说中称, 验证⼯程(verification engineering)是未来的职业[].
1.1.4 以可验证软件为⽬标的多学科交叉研究(2000年~⾄今)
1999年, 在关于计算机科学技术⾯临的巨⼤挑战的讨论中, Hoare提出了验证编译器(verifying compiler)倡议(后称为verified software).经过⼏年的调研和准备, 2005年召开了第1届VSTTE(verified software:Theories, tools, experiments)会议.来⾃世界各地的专家讨论了形式规约、构建和验证⾼质量
软件的⽅法, 形成了可验证软件计划, 希望[]:(1)建⽴能够构建实际可靠的程序的设计理论; (2)建⽴⼀组⽀持上述理论的⾃动化⼯具集, 并且能扩展⾄具有⼯业化能⼒; (3)建⽴已验证的程序库, 能够在实际系统中替代未验证的程序, 并能以可验证的状态持续演化.2007年, 我国国家⾃然科学基⾦委也开展了“可信软件基础研究”重⼤研究计划[-], 形式化⽅法作为其中的重要途径来提⾼软件的可信性.经过10余年的努⼒, 形式化⽅法进⼊了硬件设计的标准流程, 也出现了验证过的编译器[]和微内核操作系统[].⼈们普遍认可了形式化⽅法对于深刻认识计算系统和提⾼软件质量的贡献.美国NITRD在计算使能的⽹络化物理系统(CNPS)、⽹络空间安全和隐私(CSP)、软件⽣产⼒、可持续和质量(SPSQ)等多个领域(PCA)突出了形式化⽅法的位置, NSF连续资助了形式化⽅法领域的⼤规模探索项⽬CMACS[]、EXCAPE[]、DeepSpec[]等.DARPA的项⽬HACMS[]利⽤形式化⽅法成功地研发了可以免于⿊客攻击的⽆⼈机操作系统和飞⾏控制软件.形式化⽅法在计算机软/硬件开发和质量保证上发挥了重要作⽤, 与⼈⼯智能相结合的程序综合、⼤数据以及与形式推理相结合的软件⾃动化重回热点前沿.此外, 形式化⽅法在⽹络安全、量⼦计算、⽣物计算等⽅向的交叉应⽤也受到了⼴泛关注.
1.2 形式化⽅法的基本体系
给出了基于形式化⽅法进⾏软件开发的基本框架.与基于模型的软件开发类似, 通过需求分析得到初始形式规约Spec1; 然后, 经过逐步求精或者转换, 得到⼀系列精化后的形式规约(Spec2, …, Specn); 最后, 可转换或综合⽣成得到系统的程序代码实现.Spec1, ..., Specn都是对系统的抽象(建模), 它们的抽
象⾓度和层次不同.
Fig. 1 Framework of formal (development) methods图 1 形式化⽅法软件开发框架整体图
中还给出了形式规约语法、语义以及形式规约之间的关系.给定形式规约Speci, 由语义函数[[_]]给出其在数学域上的形式语义[[Speci]]
(即Semanticsi).规约之间的逻辑关系(如精化关系可以描述为逻辑中的蕴含“→”)与相应数学理论(如集合论中的集合包含“⊒”)有对应关系(如, 若Spec2→Spec1, 则[[Spec1]]⊒[[(Spec2)]]).在软件开发中, 规约不必仅⽤同⼀种形式语⾔描述, 不同的规约语⾔之间的关系可以基于某个统⼀的形式理论, 例如Institutions[].
综上所述, 形式化⽅法是由形式规约语⾔(包括形式语义与模型理论)、形式规约(包括精化与综合)、形式验证、形式化⼯具等形成的⼀个整体.其中, 形式规约语⾔是基础, 形式化⽅法中, 软件制品是规约语⾔编写/变换的形式规约; 形式验证是保证开发正确性的途径, 形式语义与模型理论是联接形式规约和形式验证的数学纽带; 形式化⼯具是系统设计和开发中⾼效使⽤形式化⽅法的需要和实践.
2 形式规约
形式规约是由形式规约语⾔严格描述的系统模型或者系统需要满⾜的性质.前者是模型规约, 后者是性质规约.形式规约是形式化⽅法的基础[].在软件分析[, ]中, 动态执⾏测试或验证技术以及动态在线跟踪监控和验证也经常使⽤形式规约.
本节我们讨论形式规约语⾔及其语义的定义⽅法、形式规约和语义模型之间的关系, 并在此基础上介绍形式规约在软件构造中的应⽤.
2.1 形式规约语⾔
形式规约语⾔是指由严格的递归语法规则所定义的语⾔, 满⾜语法规则的句⼦称为合式或良定义规约(well-formed specification).
2.1.1 模型规约语⾔
模型规约语⾔利⽤数学结构描述系统的状态变化或者事件轨迹, 它直接定义所描述系统模型的结构、功能⾏为甚⾄⾮功能⾏为(如时间).模型规约给出了系统开发过程中不同抽象层次的模型, 有相应的逻辑推理系统⽀持其分解和组合, 完成不同层次间规约的转换和精化.主要包括如下⼏类.
(1) 代数规约语⾔
kinect运动
⼀个代数规约由⼀些表述类⼦(sort)的符号、类⼦之间的运算符(operation symbol)以及在多类等式逻辑(many-sorted equality logic)中的等式公理组成.代数规约的⼀个模型就是满⾜该规约的异构代数.为了语义的唯⼀性, ⼀般采取初始代数(initial algebra)为规约的语义.代数规约的优点是具有⾮常好的数学基础, 任意操作序列的计算结果可以⾃动得到、⾃动执⾏, 例如4GL(fourth generation programming languages).等式逻辑的表述能⼒有较⼤局限性, 不能表达⼀般的程序结构和⾏为.因此, 后来代数描述中引进了带归纳的⼀阶逻辑, 同时引进了⽀持偏函数和⼦类, 模块化结构和模块组合的架构机制, 形成了⼀个通⽤代数规约语⾔(the common algebraic specification language，简称CASL)[].其他的代数规约语⾔还有OBJ[]、PLUSS[]、Larch[]等.代数规约对程序设计理论和软件⼯程影响⾮常⼴泛, 例如早期的抽象数据类型[], 后来的⾯向对象程序设计[, ]、ML等函数式程序设计语⾔[], 等等.
(2) 结构化规约语⾔
早期的结构化模型规约语⾔有VDM-SL[]、Z Notation[, ]等.VDM包括数据类型的规约和程序结构(即模块)的规约.数据类型的规约定义具有该类型的数据以及数据上的操作, 由⼀阶谓词逻辑描述数据的范围约束以及操作需要满⾜的约束.⼀个模块的规约说明程序变量及其类型以及⼀组过程或函数.过程和函数的功能约束由Floyd-Hoare逻辑来定义.VDM定义了模块的组合机制.Z-语⾔的Z-模式(Z-schema)可以描述数据类型和程序功能, 并统⼀使⽤⼀阶谓词逻辑描述集合、函数和关系, 故⽽其逻辑基础是⼀阶谓词逻辑和集合论.Z-语⾔的模块组合机制与VDM 相似.VDM和Z都是以精化为核⼼的规约语⾔, ⽀持软件
从需求规约到代码规约的⾃顶向下的瀑布开发过程模型.由于⼀阶逻辑包含在规约语⾔中, 所以可以描述模型规约需满⾜的性质.如果规约蕴含该性质, 则该归约满⾜此性质.因此, VDM和Z也⽀持包含分析验证的V型开发过程模型.
为了提供⾯向对象的软件规约和精化, VDM扩展到VDM++[], Z扩展为Object-Z[].在VDM和Z的基础和思想的影响下, 为了处理交互的分布式软件和基于服务的系统, 在类似基于数据状态的VDM和Z的静态规约语⾔中引进了事件和状态迁移⾏为, 发展了⼀系列的规约语⾔, 包括
B[]、Event-B[]、Alloy[]、JML[]和rCOS[]等, 这些规约语⾔都有明显的软件结构描述, 其中, JML和rCOS直接使⽤了现代⾼级程序语⾔的结构机制表⽰软件架构, 例如⾯向对象的继承和基于构件的软件界⾯和连接器(connector).
(3) 进程代数(演算)
为了设计开发并发和分布式系统, 出现了CCS[]、CSP[]、ACP[]等进程代数(演算).CCS和CSP都最⼤限度地将并发通信系统的数据状态和数据计算功能抽象掉, 集中描述通信和同步以及⼆者之间的关系, 是基于事件的规约语⾔.CCS规约是⼀个CCS语法定义的表达式, 语义是通过结构操作语义来定义表达式描述的通信进程的⾏为演化.这样定义的CCS表达式的状态迁移规则构成了推导CCS表达式之间各种等价关系的形式系统, 这些等价关系可以表⽰成不同的互模拟(bisimulation)关系.CSP有⽐较丰富的程
序语⾔因素, 例如外界选择、内部选择、同步并发等.CSP定义了⼀系列不同抽象层次的指称语义, 按表达能⼒递增的顺序有轨迹语义(trace semantics)、失效语义(failure semantics)和失效-发散语义(failure-divergence semantics).后来, CSP也有了完整的操作语义理论.基于进程代数的规约具有⾮常好的结构特征, 适合对复杂系统, 特别是并发、并⾏和分布式系统进⾏建模.
为了处理并发系统的其他特征, 如信息安全、移动、实时、混成、概率和随机, 这些并发模型均进⾏了各种扩充.例如, 为了处理实时系统, Reed和Roscoe扩充CSP到实时系统, 建⽴了Timed CSP[]; 为了处理混成系统, 何积丰和周巢尘等⼈将CSP扩充到混成系统, 建⽴了混成CSP[-].再如：为了处理移动计算, Milner提出了π-演算[], 后被Cardelli和Gordon进⼀步扩充为Ambient-calculus[]; 为了处理信息安全, Abadi等⼈将π-演算改进成spi-演算[]; 等等.Milner试图使⽤范畴论统⼀这些并发计算模型, 提出了Bigraph理论[].
(4) 基于迁移系统的规约
迁移系统可以⾃然地表⽰系统的⾏为.典型的基于迁移系统的规约语⾔有Petri⽹[]和Statecharts[]等.基于迁移系统的规约语⾔往往有图形化表⽰, 称为可视化规约语⾔.Statecharts⽤Higragh进⾏形式定义, 图的节点代表系统执⾏的状态, ⽽⼀个节点到另⼀个节点的边表⽰从⼀个状态到另⼀个状态的迁移, 可将模型转化为规则形式定义, 构成⼀个推理系统.由于其执⾏模型是抽象机, 这样的图形语⾔可以构建可
执⾏的规约(executable specification)或可执⾏的模型(executable model), 能够对系统⾏为进⾏仿真、测试.它们经常作为时序逻辑的解释(模型)使⽤, 可以⽤时序逻辑进⾏规约和证明其性质, 也可⽤算法判定其建⽴的模型是否满⾜⼀个时序逻辑公式.结果可以作为系统早期设计验证的依据, 以便尽早发现设计错误.但是这种形式规约组合性较差, 不容易对复杂系统建模.
北京网络安全大会
为了对⾮功能性需求建模, ⼈们对标记迁移系统进⾏了各种扩充.以⾃动机为例, 其后续扩展包括：时间⾃动机[]、混成⾃动机[]、概率时间⾃动机[]、随机混成⾃动机[], 等等.⽽且这些模型不再局限于计算机领域, 已经⼴泛应⽤于控制、⽣物、物理、化学等诸多领域.
2.1.2 性质规约语⾔
性质规约语⾔基于程序逻辑系统, 通过逻辑公式来描述⼀组性质以定义所期望的系统⾏为.性质规约不直接定义系统的具体⾏为.基于性质的形式规约偏向于说明性的, 逻辑约束往往是最⼩必要的, 以给出较⼤的实现空间.Lamport指出, 系统需要满⾜的性质可以分成两类[]：安全性质，即不好的事情从不发⽣; 活性, 即好的事情⼀定能够发⽣.Alpern和Schneider证明, 任何性质均可以表⽰成这两种性质的交[].
顺序程序设计早期的程序逻辑是Floyd-Hoare逻辑[, ].Floyd-Hoare逻辑的公式形如{Pre} P {Post}, 其中, Pre和Post是⼀阶逻辑公式, 分别称为前、后置断⾔; P是程序.通常, {Pre} P {Post}可以有如下两种解释.
a) 部分正确性：如果⼀个初始状态满⾜Pre, 且P由该初始状态的执⾏能够终⽌, 那么终⽌状态⼀定能够满⾜Post;美国在线时代华纳
b) 完全正确性：如果⼀个初始状态满⾜Pre, 那么P由该初始状态的执⾏⼀定能够终⽌, 且终⽌状态⼀定能够满⾜Post.
Floyd-Hoare逻辑的推理系统是在⼀阶谓词系统基础上添加关于程序的公理和推理规则来建⽴的.类似的规约语⾔有Dijkstra的卫⼠命令语⾔的最弱前置条件演算[].
holvoo然⽽, 这些早期的奠基性⼯作有很多不⾜之处, 如缺少对带指针和内存数据结构的程序规约机制、缺少并发程序的规约机制等等.后期有⼤量⼯作对Floyd-Hoare逻辑进⾏扩展, 形成了新的程序逻辑、规约和验证⽅法.分离逻辑[]是对Floyd-Hoare逻辑的扩展, 以⽀持带有指针和内存数据结构的程序的验证.它由Reynolds、O’Hearn、Ishtiaq和Yang等⼈在2000年前后提出, 是近年来程序规约与验证领域的最重⼤突破之⼀.它在断⾔语⾔中引⼊⽅便描述内存形状和分离特性的分离合取和分离蕴含谓词, 并在规则中将Floyd-Hoare逻辑的不变式(invariance)规则替换为框架(frame)规则.分离逻辑最⼤的特⾊是对内存和数据结构的抽象描述, 它能够更⽅便、更模块化地⽀持类似C程序的指针程序的验证.
在Floyd-Hoare逻辑的基础上, 通过引⼊⾏为轨迹的变量或不变式, 建⽴了多个并发程序的规约语⾔, 有代表性的⼯作主要包括Owicki-Gries ⽅法[, ]、Rely-Guarantee⽅法[, ]和并发分离逻辑[].与分离逻辑类
似, 并发分离逻辑对并发程序验证有很好的模块化⽀持.在其被提出之后，有⼤量⼯作对并发分离逻辑进⾏扩充, 包括将Rely-Guarantee和并发分离逻辑结合, 以⽀持细粒度并发或者⽆锁并发程序的规约和验证.基于并发分离逻辑开展的⼯作可参见Brookes和O’Hearn的综述⽂章[].除了这些针对串⾏⼀致性内存模型上的并发程序的程序逻辑外, 近年来还有⼀些⼯作对并发分离逻辑进⾏扩展, 以⽀持弱内存模型下的并发程序.⽐较有代表性的⼯作包括Vafeiadis及其团队提出的⼀系列在C11内存模型上的程序逻辑(如⽂献[]), 以证明C11内存模型(⼦集)上的程序的正确性.
为了克服Floyd-Hoare逻辑中程序和断⾔的分离及⽆法表达活性, Pratt提出在模态逻辑中使⽤程序来定义模态算⼦, 建⽴动态逻辑[].Kozen 在动态逻辑中引⼊不动点, 建⽴模态μ-演算[].在树结构上, 它的表达能⼒和⼆阶⼀元逻辑等价[, ].线性时序逻辑(LTL)[, ]和计算树逻辑(CTL) [, ]是并发系统规约和验证的常⽤语⾔.LTL和CTL的表达能⼒不可⽐较, 但都是模态μ-演算的真⼦集; Lamport提出了动作时序逻辑(TLA)[]; Moszkowski等⼈提出了区间时序逻辑(ITL)[].为了处理⼀些⾮功能性质, 这些逻辑均作了⼀些扩充.例如, 动态逻辑被扩充到混成系统, 称为微分动态逻辑[]; LTL扩充到实时系统, 称为度量时序逻辑(MTL)[]; LTL和CTL分别扩充到概率系统, 称为pLTL[]和pCTL[]; ITL扩充到实时系统, 称为时段演算(DC)[, ]等等.
2.2 形式语义学
半导体学报
形式语义学起源于对程序设计语⾔语义的研究.程序设计语⾔的语法是符号化的, 其语义就是该语⾔程序所描述的计算或者过程.在程序设计语⾔的早期, 语义⽤⾃然语⾔解释, 程序语⾔的解释器或编译器按照语义将该语⾔程序编译成计算机可处理的机器语⾔程序.这种⾃然语⾔解释的语义不精确、有歧义, ⽆法⽀持对程序正确性的严格证明和分析.为了帮助理解使⽤程序设计语⾔、⽀持语⾔标准化、指导语⾔设计、帮助开发更好的编译器以及分析证明程序的性质和程序之间的等价性, 需要对程序语⾔的语义进⾏抽象和严密的定义.为此, 出现了使⽤数学结构来定义程序语⾔语义的研究, 后扩展到各类形式规约语⾔, 形成了形式语义学.形式语义学(理论)研究形式规约语⾔语义的数学基础和构建⽅法, 提供研究形式语⾔表达能⼒、可靠性和完备性的数学⼿段.依据使⽤的数学结构和语义表⽰⽅法的不同, 形式语义研究⽅法可以分为4类，即操作语义、指称语义、代数语义和公理语义.关于计算机语⾔的形式语义的综合论著可参阅⽂献[, ].
2.2.1 操作语义
操作语义(operational semantics)使⽤抽象解释器(有时也称为抽象机或者抽象函数)定义语⾔语义, 着重模拟数据加⼯过程中计算机系统的操作.定义操作语义需要⼀个抽象机模型.最早有形式语义的语⾔是McCarthy⽤Lambda-演算定义的LISP, Lambda-演算的表达式求值过程是⽤抽象机定义的.1981年, Plotkin提出了结构化操作语义[]作为定义程序设计语⾔的⽅法.⽬前最为常见的是标号迁移系统(labeled transition system), 基本想法是把程序执⾏描述成标号迁移系统, 其中的状态为程序执⾏期间任意时刻
观察到的变量取值, 迁移关系规定如何从⼀个状态迁移到下⼀个状态, ⼀般定义为⼀组迁移规则, 每条迁移规则对应⼀个语句, 称为标号.⼀条语句的语义是由⼀组以其为标号的规则定义; 标号规则具有组合性, 即, ⼀个复合语句的规则可以由其成分语句的规则组合⽽成.
操作语义是最早使⽤的形式语义⽅法, ⽤来给出顺序程序的语义, 此时, 状态均是⼀些简单的数据结构, 迁移关系⼀般都是确定的、离散的, 也不需要考虑标号间的通信和同步.为了定义复杂程序的操作语义, 例如⾯向对象程序、并发程序、实时程序、概率程序、混成系统等, ⼈们对迁移系统进⾏了各种扩充, 或扩充它的状态, 或扩充它的迁移关系, 亦或两者同时扩充.例如, 为了定义⾯向对象程序, ⼈们扩充了程序状态, 引⼊堆和栈等复杂数据结构[]; 为了处理并发程序, ⼈们扩充了标号迁移关系, 允许使⽤标号描述通信和同步[]; 为了描述概率和随机程序, 允许以给定的概率或者随机选取迁移规则[]等等.
操作语义基于抽象机, 与计算机最为接近, 可描述实现⽅⾯的执⾏细节, 操作性⽐较强, 适合于开发语⾔编译器以及编译优化的应⽤.在语义中，状态是被直接表⽰和操作的, 也⽐较适⽤于形式验证中基于状态搜索的模型检验⽅法⾥的语义模型.然⽽, 在⼤规模或⽆穷状态的系统中, 抽象机上的推理系统⽐较弱, 不易进⾏基于演绎推理的形式验证.
2.2.2 指称语义
指称语义(denotational semantics)将语⾔的基本语法成分解释成为数学对象(称为指称), ⽤数学对象上
的运算来定义语⾔的语义.论域理论是指称语义的数学基础, 讨论各种语⾔成分的指称的数学结构, 并提供数学⼯具, 从⽽在各种数学结构之上定义语⾔语义和推导语⾔成分特性.例如, 将程序语⾔的基本语法实体的指称定义为程序状态空间上的函数和泛函, 复合语法实体的指称由构成它的⼦成分的指称复合得到.
建⽴指称语义的⾸要任务是确定⼀个相应的论域理论, 即确定程序语⾔的解释域[].处理不同的计算现象需要不同的语义, 例如, 可以定义不关⼼是否停机的顺序程序的语义, 也可以定义需要刻画停机的语义.显然, 不同的语义需要不同的论域.以CSP为例, Hoare等⼈提出了CSP的迹语义模型、失效-发散-迹语义模型等[, ], 这些语义的区别在于失效-发散的语义可以刻画程序死锁以及活锁, 从⽽分析系统的活性.论域理论的研究随着程序对象的不同⽽不断地发展着, 例如, 针对Timed CSP, ⼈们扩充了迹语义模型和失效-发散-迹语义模型, 分别提出了带时间戳的迹语义模型和带时间戳的失效-发散-迹语义模型[, ].
指称语义的论域理论具有较多可利⽤的数学性质, 有利于探讨不同语义论域及不同语义间的关系, 特别是与公理语义和操作语义间的关系.论域表⽰理论讨论了不同语义论域间的关系, 提供了不同语⾔形式语义间的关系[]; Hoare和何积丰基于⼀阶关系演算提出了程序统⼀理论(unifying theories of programming, 简称UTP)[], 其基本想法是, 通过伽罗⽡连接(Galois connection)给出同⼀语⾔不同语义间的转换关系.指称语义可以较好地⽀持形式规约的精化.
2.2.3 代数语义
代数语义(algebraic semantics)⽤代数结构来定义计算机语⾔(特别是代数规约语⾔)的语义, 是在抽象数据类型的基础上发展起来的[].在抽象数据类型中, 基调是⽤代数结构描述数据类型的语法(类⼦和类⼦间的运算), 运算的推导规则⽤⼀组公理(等式或者条件等式)描述, 这样, 满⾜这组公理的模型就是这个抽象数据类型的⼀个代数语义(称为∑-代数, 其中, ∑是基调).基于代数语义, 可以利⽤模型论和范畴论⽅法来推理该语⾔的程序性质.
抽象数据类型将数据对象及对象上的操作封装、数据类型的特性与实现分离, 具有模块化和可复⽤的性质.它与软件开发过程匹配⽐较⾃然,⾸先设计较⼩的抽象数据类型, 然后逐步扩充形成较⼤的抽象数据类型体系; 这个过程中, 抽象数据类型间可讨论层次⼀致和充分完备等性质.⼀个抽象数据类型可能有多个语义模型, 其中, 初始代数(initial algebra)和终结代数(terminal algebra)在∑-同构意义下都分别唯⼀, 采⽤初始(终结)代数模型作为语义的⽅法称为初始(终结)语义⽅法.抽象数据类型基始完备的描述可以唯⼀地扩充为相对完备, 原描述的终结模型恰好就是其极⼤扩充的初始模型, 表明了初始代数语义与终结代数语义之间的内在联系[].把⼀个规约或程序视为抽象数据类型时, 就有了它的代数语义.对于规约或程序, 可能对某些输⼊是⽆定义的, 故定义了偏抽象数据类型和偏∑-代数.另外, 在处理程序开发中, 两个不同的程序会有相同的执⾏效果, 相应的代数语义要处理好等价的问题.
代数语义与代数规约的关系密切, 主要⽤于解决基于代数规约的形式化开发中程序正确性的推理, 抽象程度⽐较⾼.如果将等式看作是从左⾄右的重写规则, 代数规约就以项重写的形式可执⾏, 成为了⼀种可
执⾏规约.
2.2.4 公理语义
公理语义(axiomatic semantics)直接使⽤形式逻辑来描述程序的语义, 其基本思路是, 在已有的形式逻辑系统的基础上增加所有程序必须满⾜的基本命题(程序公理).每个程序的基本语句都有⼀组公理和推理规则, 它们与断⾔逻辑⼀起构成程序逻辑的证明系统.程序性质的规约和验证就可直接在该形式系统中进⾏.程序逻辑的表达能⼒、可靠性、完备性以及可判定性都可归结为数理逻辑上的元性质, 程序逻辑的解释模型通常就是程序语⾔的指称语义或操作语义.
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议