一、历史背景 多年来一直困扰程序技术研究领域(2)
2013-07-03 01:06
导读：既是[ylaflna—Pnueli意义下的线性时间时序逻辑系统又是一程序语言。事实上，它是一系列化语言族(XiliehuaYuyanZu) 它以统一的程序框架表示串型或并发的过程
既是[ylaflna—Pnueli意义下的线性时间时序逻辑系统又是一程序语言。事实上，它是一系列化语言族(XiliehuaYuyanZu) 它以统一的程序框架表示串型或并发的过程性算法、抽象描述及产生式规则，还可以表示常见高级语言及多种图形语言(如数据流图，PAD图，Petri网等)的操作语义。其基本结构称为单元，具有如下的形式下面讨论几个问题(1)形式语义方法很多，为什么XYZ系统独选时序逻辑?关于时序逻辑的优点，L．Laml~t在1983年FFLP巴黎大会上已谈了很多，此处不拟一一重复．我只想指出如下的事实：不但一般程序工作者对一阶逻辑都比较熟习，而且，事实上时序逻辑中新增加的算子，都与常见高级语言中某些结构有直接的对应，比如下一时刻算子。$O”对应着状态转换的一步，二目算子。$u”与。$W”事实上直接与循环结构相对应，而终于算子“()”则对应着过程。所以，与其它形式化理论相比，时序逻辑这一形式化理论对一般程序工作者说接受起来较为自然。(2)在时序逻辑系统中·xY'Z／E有何优点?人们对时序逻辑的批评往往集中在一点，即认为时序逻辑描述令人难懂、难以验证 事实上，就单一的时序算子讲其涵义是比较易懂的，这里所谓难懂难证，我认为主要是指用多层嵌套的时序算予表示复杂的性质而盲·而XYZ／E中引入的单元中，每一条件元只允许出现一层时序算子．不允许嵌套，故并不存在难懂的问胚 近年来．在国外颇受重视的Chandy—Misra的UNITY中“性质”也是用一层时序算子来表示的 不过．由此又产生另一问题t经过这样的限制之后，XYZ／E中的单元是否仍能有一般时序逻辑公式同等的表示力?我们已经证明，存在一机械的方法将任给的一时序逻辑公式转换成等值的XYZ／E中一组单元 因此，XYZ／E中单元具有足够强的表示力。XYZ／E的另一特色，即用统一的单元框架可以表示出申型的或并发的过程性算法、抽象描述及产生式规则·此外．还可表示出常见高级语言及图形语言的操作语义。这一功能是一般时序逻辑公式所难以做到的。(3)在前面谈到XYZ／E的单元框架可以表示出多种程序结构，这一特色在程序设计方法论方面有什么重要意义?(a)逐步求精方法是一由抽象描述到可有效执行的算法程序的多层转换过程，因此，在中间各层中必然出现抽象程度逐渐减弱而程序细节逐渐增加的程序 这不同层次的程序如用不同语言来描述，则将遇到一个问题，即如何验证(甚至说明)其语义一致性?由于这个原因，经过多年研究，专家一致承认，还是用统一的语言表示各层的描述为好。但到现在止．除XYZ／E外，尚未见到另一逻辑语言能做到这一点。故这种表示力正是XYZ／E的长处所在。(b)近数年来，基于知识的程序设计颇受人注意。在这样的程序中必然需要将表示算法的部分与表示知识的部分渗合运行。显然． 如果能用统一的语盲及统一的计算模型来表示这两类程序， 不但会增加程序的可读性与可理解性，而且也易于讨论这种程序的性质。据知，在逻辑语言中能做到这一点的尚属少见。(c)由于XYZ／E能表示常见高级语盲及图形语言的操作语义，故可从它们直接自动生成表示其语义的XYZ／E文本。这一特色即使得这三类语言可相互沟通，从其一可得到其它，这一点在软件工程环境中有重要意义 比如说， 为了讨论数据流图分解前后的语义是否一致，不必从图形上讨论， 只要根据其相应的XYZ／E语义文本来讨论即可。这就大大增强了图形语言的性能。由于XYZ／E具有这种统一性．使不少专家相信，XYZ／E很适于作新型计算机的核心语言t XYZ／E是最先讨论这种统一性的语言。近年来． 已有不少人开始注意到这种范型统一性的重要意义。
本文来自中国科教评价网 三、软件工程环境
XYZ系统以上述时序逻辑语言XYZ／E为基础，由多种软件工具与环境组织成一协调的系统．以支撑多种程序设计方法和方式 总的讲．其中子系统可分支撑逐步求精方法设计可重用软件及支撑不同语言问的形式转换二类逐步求精方法又可分成二种：(I)每一步对原有描述进行组合性(即结构化)分解，其每一步分解并不改变原来的总体结构，只是将其中某些部分予以精化I(Ⅱ】每一步精化都是在上一步的基础上对解题方法作出新的决定，然后再根据此新的决定由非形式化描述逐渐过渡到形式化描述。因此，每进行这样的一步， 必须保证由于该步新决定得到的描述与上一步描述的语义一致性。可以说． (Ⅱ)比(I)更为一般一些， (I)是(Ⅱ)的较简情形。(I)是较常用的方法，但对于某些复杂的问题．(I)的方法难以处理，需要用方法(Ⅱ)。
