补充资料：形式方法

形式方法
formal method

实际中也是不可行的。在交互式验证系统中，整个证明过程是在人的指导下进行的。系统可随时求助于人的智慧来决定下一步怎么做，因此从理论上说可以对付任何问题。但过多地要求人的干预会导致证明效率低下等问题。实际上大多数交互式工具都含有不同程度的自动化成分。 通过事后验证来保证程序的正确性，显得过于消极。不但难以措手，而且为时己晚。较为积极的办法是研究程序开发过程本身，探寻保证正确性的程序开发方法。这些方法一般是“目标制导”的，即从给定的形式规约出发，应用适当的规则，逐步推出可执行的程序。由于这些规则是保持正确性的，所得到的程序一定满足所给的规约，而无须事后另作验证。这样的程序推导(或转换)涉及到不同层次上，即从规约到程序的各种对象，因而要求对所用的规约语言与编程语言的语义在同一框架中给出。例如在“最弱前置条件演算”中，规约断言与程序语句(“卫式命令”)的语义都统一用最弱前置条件来定义。程序推导与转换在函数式与逻辑式程序设计风范中也得到深人的研究。 在直觉主义逻辑中，“证明’，必须是能行的，利用最近20年来直觉主义类型论的成果，可以将类型论中的“谓词”看作对程序的规约，谓词为真的证明即是(带类型的)补演算的项，因而可看作是函数式程序语言中的程序。这样，“程序满足规约”这句话翻译为类型论的语言就是“论据证明谓词为真”。基于这种对应关系，就可以在直觉主义逻辑系统中进行证明，而从证明中“抽取”出程序(参见基于类型理论的方法)。 近年来对实时系统形式方法的研究取得了很大进展。在实时系统中时间因素对系统的行为起关键的、甚至是决定性的作用。典型的实时系统有飞机或导弹的飞行控制系统、各类工业过程控制器、以及通信系统等。目前比较成功的用于实时系统的方法，多数是在已有的关于非实时系统的方法基础上扩充时间因素，比如在时序逻辑(线性或区间)中引人时间参数、或在传统的进程代数中增加表示时间的算子。一般要求这种扩充是保守的，即在原形式系统中为真的事实在扩充后的系统中仍然为真。泥成系晚是一类特殊的实时系统，其特点是既随时间而连续变化，又受离散突发事件的驱动。对混成系统形式方法的研究方兴未艾。 形式方法的另一个重要应用领域是系统的分解与集成。大型软件系统由成千上万个模块组成，这些模块又按一定的原则组织成一些子系统。模块和子系统的对外界面与版本信息，以及模块、子系统之间的调用、联结关系，都可以形式地加以描述。这种系统结构描述一般在系统设计阶段进行。在系统集成阶段可以利用这种结构描述进行界面与版本一致性检查，也可以自动地从模块库产生最终的可运行系统。实际上，几乎所有的软件开发环境都不同程度地提供这方面的支持。

说明：补充资料仅用于学习参考，请勿用于其它任何用途。