如一个简单的一元谓词:
定义1:树都有树叶。
定义2:A是树;
定义3:B与A是同一类植物;
则可知B是树并且有树叶。
其实谓词演算就是对于数学包含关系的判断。
如果体现在编程中,就是变量的对比,转换,替换和传递等。
1950年代—1960年代初,手工艺式的程序设计方法,高德纳把程序称为艺术品。
1960年代末—1970年代初,出现软件危机:一方面需要大量的软件系统,如 *** 作系统、数据库管理系统; 另一方面,软件研制周期长,可靠性差,维护困难。编程的重点:希望编写出的程序结构清晰、易阅读、易修改、易验证,即得到好结构的程序。
1968年,北大西洋公约组织(NATO)在西德召开了第一次软件工程会议,分析了危机的局面,研究了问题的根源,第一次提出了用工程学的办法解决软件研制和生产的问题,本次会议可以算做是软件发展史上的一个重要的里程碑。
1969年,国际信息处理协会(IFIP)成立了“程序设计方法学工作组”,专门研究程序设计方法学,程序设计从手工艺式向工程化的方法迈进。 1968 年,结构化程序设计方法的研究。Dijkstra 提出了“GOTO是有害的”,希望通过程序的静态结构的良好性保证程序的动态运行的正确性。
1969 年,Wirth 提出采用“ 自顶向下逐步求精、分而治之” 的原则进行大型程序的设计。其基本思想是:从欲求解的原问题出发,运用科学抽象的方法,把它分解成若干相对独立的小问题,依次细化,直至各个小问题获得解决为止。 1967年,Floyd 提出用“ 断言法” 证明框图程序的正确性。
1969年,Hoare 在Floyd 的基础上,定义了一个小语言和一个逻辑系统。此逻辑系统含有程序公理和推导规则,目的在于证明程序的部分正确性,这就是著名的Hoare逻辑。他的工作为公理学语义的研究奠定了基础。
1973年,Hoare和Wirth把PASCAL语言的大部分公理化。
1975年,一个基于公理和推导规则的自动验证系统首次出现。
1979年,出现了用公理化思想定义的程序设计语言Euclid。
1976年,Dijkstra提出了最弱前置谓词和谓词转换器的概念,用于进行程序的正确性证明和程序的形式化推导。
1980年,D.Gries综合了以谓词演算为基础的证明系统,称之为“程序设计科学”。首次把程序设计从经验、技术升华为科学。
1974年,人们利用模态逻辑验证并行程序的正确性。
关于程序正确性证明的争论:
怀疑和反对派,理由:首先,形式证明太复杂,谁能够保证证明本身没有错误呢!其次,程序写好后再证明其正确性,相当于“ 马后炮” ,即错误已经铸成,证明何能补救?
折中的方案:编写程序,边考虑证明。即程序设计与正确性证明同时并行考虑。 利用Dijkstra 的谓词转换器及其演算规则集合,可以推导出正确的程序。
利用程序变化构造正确的程序。它对程序应用一连串的保护正确性的变换规则,最终得到可执行的程序。程序变换是1970年代以来,“程序设计方法学” 研究的重要方面,是程序设计自动化很有希望的途径之一。递归程序变换是这一时期的最有意义的成果。 如Burstall 和Darlington 的递归程序变换系统等。
逻辑程序设计和函数程序设计代表一种新的研究方向。Prolog是以谓词逻辑的子集(Hoare 子句)为基础的一种形式系统。Prolog 的执行过程就是执行逻辑上消解算法的过程。 抽象数据类型是程序设计方法学中一种极为重要的方法。人们把它誉为程序设计方法学发展史上的一个重要的里程碑。
Fortran:由一个主程序或一个主程序与若干个子程序组成。ALGOL:巴乎斯范式BNF来描述言的语法。还提供动态数组和过程的递归调用。
COBOL(COmmon Business-Oriented Language)是一种面向事务处理的高级语言。目前COBOL语言主要应用于情报检索,商业数据处理等管理领域。
Pascal语言是一种结构化程序设计语言,过程可以是嵌套和递归的。
C语言:兼顾了高级语言和汇编语言的特点,简洁,丰富,可移植。直接访问 *** 作系统和底层硬件,C在系统应用和实时处理应用的开发中成为主要语言。
C++:是在C的基础上增加了类机制,使其成为一种面向对象的程序设计语言。
Java,目的是用于开发网络浏览器的小应用程序.
分类:
1.命令式程序设计语言是基于动作的语言,Fortran,Pascal,C
2.面向对象的程序设计语言,模拟领域发展起来的Simula,C++,Java,smaltalk,
对象,类,继承,是面向对象的三大特点。
3.函数式程序设计语言是一类似λ-演算为基础的语言,基本要领来自于LISP(1958年为了人工智能应用而设计的语言).函数是一种对应规则(映射),它使定义域中每个元素和值域中唯一的元素相对应。 LISP程序和数据等价.数据结构可以作为程序执行,程序可以作为数据修改.
4.逻辑型程序设计语言,以形式逻辑为基础的语言,其代表是建立在关系理论和一阶谓词理论基础上的PROLOG(Programming in Logic).关键 *** 作是模式匹配。有很强的推理功能,适用于书写自动定理证明,专家系统,自然语言理解等问题的程序。
http://blog.csdn.net/mShopping/archive/2008/10/14/3073176.aspx
欢迎分享,转载请注明来源:内存溢出
评论列表(0条)