通信的顺序进程及其研究

通信的顺序进程(Communicating Sequential Processes)是C.A.R.Hoare教授提出的,简称为CSP,他希望以此作为分布式程序设计的基本机制。 本文以“通信的顺序进程及其研究”作为总称,共分六篇。第一篇以总称为名,介绍CSP的目标及一个CSP式的应用式语言(Applicative Language)。第二篇名为“通信进程的确定性语义学”,该文中给出了这个语言的一种语义,这种语义不考虑CSP中允许的很多非确定现象。语义中同时使用了指称方法(Denotational Semantics)和公理化方法(Axiomatic Semantics)。第三篇为“通信协议的部分正确性”。该文用CSP构造了一个HDLC协议,并用第二篇文章中提供的方法,证明了这个协议的部分正确性。在证明过程中,作者引入了一个类似于顺序程序设计中最弱前提(Weakest Precondition)的最弱环境(Weakest Environment)概念。第四篇中,在一种层次通信结构中,详细地讨论了最弱环境这一概念,文章的名称为“通信进程的最弱环境”。最后两篇讨论CSP的非确定性语义,这种语义考虑了CSP的各种允许的非确定行为。CSP的非确定性语义是用操作语义学(Operational Semantics)和公理化语义学同时给出的。标题为“通信进程的非确定性语义学(上)”及“(下)”。     

程序正确性证明的形式技术——J.Schwartz教授来华讲演记录

美国纽约大学柯朗数学科学研究所计算机科学部主任 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年底整理而成。其中第三部分变形的形式化由洛阳石油设计院陶志成负责整理,其余各部分则科学院计算所周巢尘整理。整理过程中得到唐稚松、吴允曾同志的关心和帮助。     

结构式时态语义

本文定义了程序语言的一种结构武时态语义,即将程序语言中的语句解释为时态逻辑中的公式,并使这种解释保持语言的结构。本文的续篇名为“程序推理”,将讨论在这种语义基础上的程序推理问题。     

通信协议的设计

在[5],[6]中,我们陈述了一个用于分布式程序设计的语言原型,这个原型是基于Hoare所提出的通信顺序进程的;并且建议用通道谓词作为分布式程序的功能描述;在发展这个语言的公理语义的同时,也给出了证明程序特性的一种形式途径。本文中,我们将使用上述工具讨论通信协议的结构式设计。本文原拟名为“通信协议的部分正确性”。     

程序模式和谓词演算

本文给出了AEA公式的不可满足问题至程序模式的终止问题的归约,从而证明了程序模式基本特性的不可判定性,并使用谓词演算的判定方法,证明了一类广义Ianov模式的基本特性是可判定的。文末讨论了定理的机器证明和程序模式特性机器证明的本质区别。一般情况下,后者不必历经整个Herbrand域,而仅需考虑一个一致有界分叉的无穷树状子域。另外也毋需讨论通常的可满足性问题,为此,本文中提出了通路可满足的概念。     

国外操作系统的若干研究动向

一、同步机构进程之间共享资源时,则发生同步问题。同步问题是导致操作系统复杂性的重要原因之一。因此当前花相当大的力量来研究这一问题,特别是扩充已有的同步机构和探索新的同步机构。目前同步机构主要有以下几种: 1.信号量 Dijkstra在1968年前后提出了信号量概念及P、V操作,并应用于THE系统[Dij68 B],获得了普遍重     

形式语义学引论 操作语义学

1.引言(Introduction) 程序设计语言的实施者是按照语言的语义在具体的计算机系统中编制语言的解释程序或者编译程序的。但反过来看,语言在任何计算机系统中的任何一种实施一旦完成,那末对这个计算机系统而言,语言的含义也就完全确定了;也就是说,语言的一种实施可看作是语言语义的一种定义。用语言的实施作为语言的语义定义,也就是将语言成分所对应的计算机系统的操作作为语言成分的语义,故这种语义称作操作语义。当然语言的语义应该是标准的,不应依附于一个特定的计算机系统,一种具体的实施。因此操作语义学中使用抽象的机器和抽象的解释程序来定义语言的语义。     

管程的验证和Hoare系统的不完全性

本文讨论管程(Monitor)的验证技术。指出了Howard的证明规则是不一致的,并证明了不存在验证管程的一致和完全的正规Hoare系统。Ciarke证明了,对于功能很强的语句——递归过程,Hoare系统是不完全的;本文的结果表明Hoare系统对并发现象中复杂的控制转移结构也是不完全的。     

通信进程的确定性语义学

在“通信的顺序进程及其研究”一文中,给出了一个以输入输出操作和并行组合为基本要素的语言原型。本文中提出这一语言的两种语义,指称语义(Denotational Semantics)和公理化语义(Axiomatic Semantics)。但这两个语义中都回避了语言可能具有的某些不确定性,这一问题将留待以后解决。     

并发进程系统正确性的验证图式

并发进程系统正确性的验证,比之顺序进程正确性的验证有其特殊意义。并发系统的运行,在执行序列这一级上是非决定的,通常的调试手段,很难暴露系统中依赖于执行序列的那类错误。因此并发系统正确性的验证,在三种不同水平上都是有价值的:完全形式化的形式演绎系统;半形式化的数学证明;或者有效的检查调试方法。 并发系统运行的非决定性,也极大地增加了验证的复杂性。在证明系统具有某个性质时,粗略地说,就是要证明这个系统的所有执行序列都具有这种性质。一个顺序进程,从给定的初始状态出发,只有一个可能的执行序列;但是多个并发进程的可能执行序列则往往是无穷多个。由于这种复杂性禁锢了人们的智力活动,使得一些简单的事实,人们也很难将其严格证明。系统中存在的问题,事后看来即使是一些很明显的问题,也会被这种复杂性掩盖起来,长时间不被发现。