文档介绍：,。瓤翁产壕荨∥差鬟。独创性声明学位论文版权使用授权书本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。据我所知,除了文中特别加以标注和致谢的地方外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含为获得或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表学位论文作者签名:签字日期:年本学位论文作者完全了解江西师范大学研究生院有关保留、使用学位论文的规定,有权保留并向国家有关部门或机构送交论文的复印件和磁盘,允许论文被查阅和借阅。本人授权江西师范大学研究生院可以将学位论文的全部或部分内容编入有关数据库进行检索,可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。C艿难宦畚脑诮饷芎笫视帽臼谌ㄊ示谢意。月导师签名:日
『●瘛甶亍危#
摘要从上世纪六十年代起,随着大型软件的快速发展,人们对软件质量的要求起来越高,尤其是对软件的氯沸砸G蟆<扑慊缥H繁H砑柿坑绕涫侨砑高可靠性方面提出了许多新的理论研究,程序正确性证明就是其中之一,程序正确性证明就是采用严格的数学方法评价一个程序是否达到了预定的性能。但是在证明程序正确的过程中由于要涉及大量的数学符号和数学相关理论知识使得程序验证人员需要花费一定的时间和精力去掌握这些知识。而且由于涉及到数学理论即使验证一个很短的程序也需要比较繁琐的验证过程,造成往往证明过程比要证明的程序要复杂很多的情况,这些种种不利条件使得依靠手工去证明程序正确性就可能产生许多不良的后果。为了克服手工对程序进行正确性验证程序所导致的不良后果,许多计算机科学家丌始利用机器去自动验证程序来逐步降低人工下预程序验证的过程,最终的目的是将程序正确性验证走向完全自动化。根据的最弱自订置谓词理论,对于程序绻苤っ鳎篞—癝”,则能断定程序『贰U腔诖死砺郏疚难芯孔魑狿平台的一个辅助工具部分,目标是丌发一个自动计算程序的最弱前置谓词的系统,减少程序正确性验证的人工干预,在已知琑的情况下自动求解出最弱前围绕这个宗旨本文做了如下工作:⒃谏羁汤斫饬薉钊跚爸梦酱实牡幕∩咸岢隽俗远扑鉇语言最弱前置谓词的算法。⒀∪×巳舾葾绦蚪惺匝椋笛榻峁砻鳎低吵醪绞迪至俗远计算最弱前置谓词的功能。⒊⑹越獶钊跚爸梦酱首远善髡系絇平台,使其成为囊桓龈ㄖぞ撸荒芄挥行У闹С諴平台。后期的工作包括完善系统的各项功能;进一步提高系统的可靠性和健壮性;加强对复杂性算法和经典数学问题算法的分析和求解。关键词:程序正确性证明,椒ǎ珹镅裕珼钊跚爸梦酱剩器置渭词。●
琲曲—癝”,;珺,,,,。,琍,琓。。,.。瑃,琑
琍,,。,;籈:珿却
椒ǎ疨平台简介⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⒉街琛第三章最弱前置谓词计算方法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.最弱前置谓词概述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.赋值语句计算⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.条件语句计算⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯‘循环语句计算⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯过程调用语句计算⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第四章最弱前置谓词生成器的设计⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。系统设计原则⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。系统总体设计⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..低巢愦谓峁股杓啤.●
.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯...⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。系统总体功能实现描述⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.史ǚ治瞿???椤低秤τ谩第六章总结与展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯总结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.展望⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。参考文献⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯致谢⋯⋯..⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯⋯⋯.⋯⋯⋯⋯⋯..⋯⋯⋯⋯⋯⋯⋯攻读学位期间参与的科研项目⋯⋯⋯⋯⋯⋯⋯..
第一章言研究背景与研究现状和等;法国国家计算机科学及控制引随着计算机应用的日益广泛,需要开发的软件规模越来越庞大。上千万行的大型系统软件及百万行的应用软件已经屡见不鲜,然而软件质量却一直是所有人头疼的问题,随着规模的扩大,对于质量的保证已经成为一项异常艰苦的