| 摘 要： | 美国纽约大学柯朗数学科学研究所计算机科学部主任 J.Schwartz 教授,应中国科学院计算技术研究所邀请,于一九七七年九月十七日至十月三日偕夫人共同在京讲学。讲学内容之一为“程序正确性证明的形式技术”(Formal Techniques for Proof ofProgram Correctness),共分十讲,每讲约一小时半,写有提纲。要求听讲者事先阅读 Z.Manna 所著《计算的数学理论》(Mathematical Theory of Computation)。及 J.E.Rubin所著《数学家所用的集合论》(Set Theory for Mathematicians).临行前留下他本人所著《关于㊣程序的技术》(On correct-Program Technology)以及和M.Davis合著的《定理验证系统和证明校验系统的元数学可扩充性》(metamathematical Extensibility for Theorem Verifiers and Proof-Checkers).在证明程序正确性的研究中,有若干不同的算什么。其中之一是致力于研究保持程序正确性的加工(manispulation)和组合(Combination)规则,以便从一个正确的程序出发(例如,从一个则高级语言写成的,已被验证为正确的程序出发),经上述规则得到其他正确程序(如目标程序)。Schwartz教授认为这是一个重要的途径。他以SETL语言书写的程序为研究对象,并提出了接近于Hoare系统的形式化验证方法。他认为使用SETL高级语言,不但使程序编写得简短,而且在描述归纳断言(inductive assertion)方面也是自足的。Schwartz教授也研究了程序的加工和组合规则,称这为变形规则(transformation rule).另外,由于人工证明程序正确性的过程中,仍然难免错误,因这提出证明验证系统问题,即建立一个计算机化的系统,自动验证人们给出的证明是否正确,他介绍了自己和Davis在这方面的工作。Schwartz在京讲学期间,还作过两次大型讲演,内容之一为“程序设计的非确定型方法：用途及其实现”(Programming Nodeterminism:Use and implementation).因验证系统的程序语言中允许出现非确定的选择算子,故将讲演附在本文后一起发表。本文根据讲授提纲和听课笔记,并参照两篇专著于1977年底整理而成。其中第三部分变形的形式化由洛阳石油设计院陶志成负责整理,其余各部分则科学院计算所周巢尘整理。整理过程中得到唐稚松、吴允曾同志的关心和帮助。
|
