首页计算机书籍程序设计时序逻辑程序设计与软件工程 下 软件工程方法与工具_唐稚松等著_7030099281
face

文档

881

关注

0

好评

0
PDF

时序逻辑程序设计与软件工程 下 软件工程方法与工具_唐稚松等著_7030099281

阅读 526 下载 0 大小 1.42M 总页数 21 页 2023-03-19 分享
价格:¥ 10.00
下载文档
/ 21
全屏查看
时序逻辑程序设计与软件工程 下 软件工程方法与工具_唐稚松等著_7030099281
还有 21 页未读 ,您可以 继续阅读 或 下载文档
1、本文档共计 21 页,下载后文档不带www.pdfdz.com水印,支持完整阅读内容。
2、古籍基本都为PDF扫描版,所以文档不支持编辑功能,即不支持文档内文字的复制粘贴。
3、当您付费下载文档后,您只拥有了使用权限,并不意味着购买了版权,文档只能用于自身使用,不得用于其他商业用途(如 [转卖]进行直接盈利或[编辑后售卖]进行间接盈利)。
4、本站所有内容均由合作方或网友上传,本站不对文档的完整性、权威性及其观点立场正确性做任何保证或承诺!文档内容仅供研究参考,付费前请自行鉴别。
5、如文档内容存在违规,或者侵犯商业秘密、侵犯著作权等,请点击“违规举报”。
席岸田孝一等)的思路较为接近。这就说明,为什么在开始阶段XYZ系统从理论界与软件工程界这两方面所得到的反应是如此的不同!特别应该一提的是日本友人岸田孝一先生,他不但对西方软件技术十分了解,而且对中国传统文化有很深的素养,因此他对XYZ系统的哲学背景的兴趣也显得特别浓厚。他不但多次邀请我到日本作为软件学术会议的特邀主题报告人讲XYZ系统的哲学背景,而且亲自在《朝日新闻》上写专文介绍XYZ系统(1995年12月4日)。文中说:“唐教授的成就之一就是花了近15年的时间成功地开发了称为XYZ的软件系统。尽管系统所采用的最基础的数学理论来源于西方,但构造此系统的基本思想却来自孔子的中庸哲学和佛教的禅宗认识论哲学。这也许可以说是东方文明对于新的21世纪计算机技术发展的一大贡献吧。”岸町这一情况当然不易为西方多数理论家所理解,而瑞士苏黎世ETH的Engeler教授及德国Braunschweig的Ehrich教授等少数理论家算是例外。在XYZ系统设计中,我之所以强调哲学思想指导,并不是出于为哲学而哲学的学院式兴趣,而是由于20世纪80年代初对国际软件理论与技术的发展潮流及其思想背景感到怀疑与忧虑所致。事实上,国际计算机科学家中有类似怀疑和忧虑的人并非少见,如斯坦福大学的D.Knuth教授就是较著名的一位①下面让我们回倾一下计算机科学技术的发展历史。众所周知,在20世纪70年代中期以前,计算机科学领域的理论与技术是紧密相联的,如形式文法(包括属性文法)及语法分析方法的研究与编译技术是相互依存的。可是自从语义形式化问题提出以来,由于这问题难度很大,希望从传统数学理论中找新的工具与方法的要求很普遍,许多有才能的青年数学家逐渐进入这一研究领域。他们在软件技术方面的根基不很深厚,但受理性主义传统影响很大,数学的职业倾向性远远大于软件的职业倾向性。从20世纪80年代以来,在这类人员集中的机构、地区与会议上,其价值标准(如脱离实用意义,单纯从理论的逻辑严密性及深度与难度对工作进行评价等)以及学术气氛也就逐渐发生了变化,从而不能不影响学科发展方向,使计算机科学理论研究日益脱离软件的现实实用性考虑而成为一种较深的数学探索。这种情况自然难被关心市场效益的工业界所接受。特别是以实用主义传统著称的美国工业界,他们虽然也很关心提高软件生产率,关心软件的可靠性与可维护性这类关键问题,但他们对日益远离工程技术实用性的形式化语义理论及规范语言的研究逐渐失去信心与兴趣,终于导致几乎完全抛弃了理论研究,而单纯从技术上找出路。他们企盼软件像硬件一样,用从技术上提高自动化水平或可重用性的途径找到提高生产率的方法。这种思路大大推动了软件工具及与之相联系的操作系统的发展,其后果是整个20世纪80年代,对于软件研究与发展来说,就是一个理论与技术相互分离脱节、各走极端的年代。这种情况在一段时间内使双方都得到一定程度的满足,理论家获得了很高的荣誉,而工业界也获得了不小的利润。可是,提高软件生产率及可靠性与可维护性等根本性问题不但没有解决,而且似乎希望日益渺茫。这种情况是否合理?这些根本性问题是否已失去意义?事实并非如此。不但美欧各国关键技术委员会①1995年他在访问Dk大学时,与我过去一位名叫金伟的学生(现在该校作博士生)谈到过我,他说:“唐教授是我遇到的惟一一位关心计算机科学在10年、0年后如何发展这个问题的中国计算机科学家。因此,我建议斯坦福大学计算机科学系邀请他来访问。”事实上,XY忆系统的设计思想正是这次访问时开始形成的]。每年一次向国家最高当局提出的报告中都将这个问题放在首位,而且甚至像微软这样一贯强调软件技术且已取得大量利润的公司也已感到,由于缺少精确语义基础,大型软件的可靠性与可维护性问题已制约他们进一步的发展,因此不久前该公司已在剑桥大学等处投入巨资开展这方面的研究。事实上,语义的精确性与技术的自动化二者是相互依存、不可分割的,而且只有紧密结合才能达到提高软件生产率的目标。因此,如果不从根本上找出理论与技术脱节的病根来辨明道路,单靠投入资金岂能解决这个问题。那么,产生这个问题的根本原因何在呢?40多年来,有关计算机科学的研究实际上是围绕以某种模型为基础的三个彼此相关的层次进行的,即计算机体系、适应该体系的可执行程序语言及表示程序抽象语义的规范语言。众所周知,4O多年来流行的计算机体系都是建立在冯·诺伊曼(von Neunn)模型上的,流行的程序语言即为适应这种机器体系的常见命令式语言(如Pascal,Ada,C,C++等)。这种模型主要的特征即为自动机状态转换机制。通俗地说,表现为变量在运行过程中可通过赋值命令(语句)改变其值,且其控制流可分解成“循环”、“分支”及“继续”等基本结构,其中尤以“循环”最具特殊的意义。由于这些特征使这种语言能高效地在冯·诺伊曼型计算机上运行。至于适应这样模型的规范语言,人们较为广泛接受的是Hoare逻辑中的由前置断言(pre assertion)与后续断言(post assertion)所表示的逻辑语义。以上三个层次对冯·诺伊曼模型的表示方式相互间是紧密关联,协调一致的。它有其优点与缺点,优点是其常见命令式语言执行效率高,为广大计算机用户所习用(特别是用循环表示重复计算),在Hoae逻辑的作用下,命令式语言的程序与由前置和后续断言表示的规范协调地联系在一起,而且对于数学水平不高的初学者来说,按照自动机状态转换方式设计一个规模不太大的程序或模块较为直观而易于掌握;其缺点是这种基于自动机状态转换的机制不够抽象,包含细节太多(赋值本身即是一种细节),不能像数学中常用的函数那样便于嵌套与连接,平常数学中许多理论与技巧(如证明技巧)不易在其中直接应用等等;而更重要的是,在这种命令式语言与规范语言的关系中,后来发现一些语义方面的难题长期找不到解决的办法。比如,常见命令式语言中递归过程(及进程)这类模块的后续条件如何表示其递归性并如何验证其正确性?更困难而又更重要的一个问题是,对于由通信进程组成的并行语句,如何表示其语义?如何验证其正确性?事实上,在冯·诺伊曼模型的框架内,惟一可行的办法是将并行语句的语义归结为该语句所包含的串型进程语义的合取,但这一命题成立的条件是语义可组合性。而事实表明,在通信的情况下这一条件可能是不成立的。因此,困难在于如何保证并行语句语义可组合性条件成立。容易看出,上述优点是工程界所重视的实用性方面的优点,上述缺点是理论界所强调的数学精美性方面的弱点,而上述困难问题则的确是冯·诺伊曼模型所面临的实质性问题。不解决这些问题必将严重影响程序的可靠性与安全性,使冯·诺伊曼模型不论从理论上还是从工程上说都将难以采用。(C.A.R.Hoae在文献[Ho2]中讨论CSP的数学模型时明确指出,他在文献[Ho2]中放弃了文献[Ho1]中的语义模型,而采用了与CCS相同的进程代数所要求的函数式模型,其中三条原因中的前两条就与这里所述的两项困难问题直接相关。)由于上述情况,从20世纪70年代末起,计算机科学领域出现寻找其他非冯·诺伊曼模型的高潮。其中最有影响的即函数式模型的研究,包括函数式机器体系、函数式程序语言,以及以递归性与函数映射为特征的基于可计算函数(包括入演算)及代数
返回顶部