一類程序終止性分析的代數(shù)方法.pdf

1、當(dāng)今時(shí)代,計(jì)算機(jī)已經(jīng)成為人們工作生活必不可少的工具。計(jì)算機(jī)及其軟件使用已經(jīng)滲透到人類活動(dòng)的各個(gè)領(lǐng)域,軟件作為計(jì)算機(jī)功能實(shí)現(xiàn)的核心要素,使得設(shè)計(jì)高可信軟件成為計(jì)算機(jī)領(lǐng)域日益關(guān)注的問(wèn)題。而軟件驗(yàn)證作為高可信軟件設(shè)計(jì)的重要部分,實(shí)現(xiàn)軟件程序的自動(dòng)驗(yàn)證將對(duì)高可信軟件設(shè)計(jì)工作具有十分重要的意義。
　　作為計(jì)算機(jī)程序設(shè)計(jì)領(lǐng)域的傳統(tǒng)研究課題,程序驗(yàn)證是研究程序正確性的理論。程序終止性問(wèn)題是程序驗(yàn)證的主要內(nèi)容,程序終止性問(wèn)題的研究突破對(duì)程序驗(yàn)證工

2、作起到十分關(guān)鍵的作用。
　　本文主要研究了程序的終止性問(wèn)題,在基于特征值的理論中提出了一類非線性的while型循環(huán)程序的終止性是可以判定的,指出該類程序的終止性與其賦值矩陣的正特征值相對(duì)應(yīng)的特征向量有關(guān),并提出判定此類程序終止性的一種新方法,既能判定程序是否終止,又能對(duì)不是所有初始值均終止的程序給出終止情況下的初始值建議。
　　文章首先簡(jiǎn)要介紹程序完全正確性的定義,程序的完全正確性是由程序的部分正確性和程序的終止性構(gòu)成。再分

3、別對(duì)程序的部分正確性和終止性的判定方法進(jìn)行論述:
　　(1)關(guān)于程序的部分正確性。
　　列舉不變式斷言,Hoare公理化和Dijkstra最弱前置謂詞變換三種判定程序部分正確性的方法。
　　(2)關(guān)于程序的終止性。
　?、僦赋龆鄶?shù)程序終止性證明方法所采用的本質(zhì)思想是判定程序遷移關(guān)系是良基關(guān)系的方法;
　?、谟懻摶谥群瘮?shù)的線性循環(huán)程序終止性分析和基于特征值理論的線性循環(huán)程序終止性分析兩種方法,歸納兩種方法的