一類程序終止性分析的代數(shù)方法.pdf_第1頁
已閱讀1頁,還剩46頁未讀, 繼續(xù)免費(fèi)閱讀

下載本文檔

版權(quán)說明:本文檔由用戶提供并上傳,收益歸屬內(nèi)容提供方,若內(nèi)容存在侵權(quán),請進(jìn)行舉報或認(rèn)領(lǐng)

文檔簡介

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

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

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

溫馨提示

  • 1. 本站所有資源如無特殊說明,都需要本地電腦安裝OFFICE2007和PDF閱讀器。圖紙軟件為CAD,CAXA,PROE,UG,SolidWorks等.壓縮文件請下載最新的WinRAR軟件解壓。
  • 2. 本站的文檔不包含任何第三方提供的附件圖紙等,如果需要附件,請聯(lián)系上傳者。文件的所有權(quán)益歸上傳用戶所有。
  • 3. 本站RAR壓縮包中若帶圖紙,網(wǎng)頁內(nèi)容里面會有圖紙預(yù)覽,若沒有圖紙預(yù)覽就沒有圖紙。
  • 4. 未經(jīng)權(quán)益所有人同意不得將文件中的內(nèi)容挪作商業(yè)或盈利用途。
  • 5. 眾賞文庫僅提供信息存儲空間,僅對用戶上傳內(nèi)容的表現(xiàn)方式做保護(hù)處理,對用戶上傳分享的文檔內(nèi)容本身不做任何修改或編輯,并不能對任何下載內(nèi)容負(fù)責(zé)。
  • 6. 下載文件中如有侵權(quán)或不適當(dāng)內(nèi)容,請與我們聯(lián)系,我們立即糾正。
  • 7. 本站不保證下載資源的準(zhǔn)確性、安全性和完整性, 同時也不承擔(dān)用戶因使用這些下載資源對自己和他人造成任何形式的傷害或損失。

評論

0/150

提交評論