目前計(jì)算機(jī)軟件的發(fā)展受著多種因素的影響,它滯后于硬件,其安全性、可靠性和穩(wěn)定性一直是人們關(guān)注的幾個(gè)重要問題。隨著軟件的大型化、模式化,以及安全性需求的日益提高,人們對(duì)軟件質(zhì)量的要求起來(lái)越高,尤其是對(duì)軟件的正確性要求。軟件質(zhì)量問題由來(lái)已久,由于在許多關(guān)鍵領(lǐng)域運(yùn)行的軟件質(zhì)量問題而引發(fā)重大損失甚至災(zāi)難并不少見。 基于調(diào)試的方法有很大的局限性。在一些經(jīng)過調(diào)試并投入運(yùn)行的系統(tǒng)程序或應(yīng)用程序中還存在著隱患。因此,為了保證程序的正確性,必須從理論上研究有關(guān)程序的正確性證明的方法。計(jì)算機(jī)科學(xué)家用完全形式化的方法來(lái)證明程序同功能歸約的一致性,保證程序的正確性。形式化證明把程序完全正確性問題歸結(jié)為部分正確性和終止性的證明。 本文提出了一種新的基于形式化理論的程序自動(dòng)驗(yàn)證方向:即在程序抽象證明中引入時(shí)間邏輯。時(shí)間邏輯是在一階邏輯的基礎(chǔ)上通過顯式地引進(jìn)時(shí)間變量而得到的一種邏輯。本文用這種邏輯描述程序設(shè)計(jì)語(yǔ)言各個(gè)語(yǔ)言成分的語(yǔ)義,驗(yàn)證程序的性質(zhì),以及軟件規(guī)范。結(jié)合利用編譯技術(shù)實(shí)現(xiàn)的編譯器,針對(duì)C語(yǔ)言類型定義、變量定義、運(yùn)算符、表達(dá)式、語(yǔ)句、函數(shù)定義及函數(shù)調(diào)用的語(yǔ)義,將源程序翻譯為時(shí)間邏輯公式。最后利用數(shù)學(xué)原理證明...

【文章頁(yè)數(shù)】：73 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
Abstract
1 緒論
    1.1 研究背景
        1.1.1 程序驗(yàn)證概述
        1.1.2 運(yùn)用編譯技術(shù)的優(yōu)點(diǎn)
    1.2 國(guó)內(nèi)外研究發(fā)展與現(xiàn)狀
    1.3 本文研究目的及主要工作
    1.4 論文章節(jié)安排
2 時(shí)間邏輯
    2.1 時(shí)間邏輯語(yǔ)言
    2.2 歸結(jié)原理
        2.2.1 子句集
        2.2.2 命題邏輯中的歸結(jié)原理
        2.2.3 替換與合一
        2.2.4 謂詞邏輯中的歸結(jié)原理
3 程序設(shè)計(jì)語(yǔ)言的公理語(yǔ)義
    3.1 類型定義的語(yǔ)義
    3.2 變量定義的語(yǔ)義
    3.3 運(yùn)算符和表達(dá)式的語(yǔ)義
    3.4 語(yǔ)句的公理語(yǔ)義
    3.5 函數(shù)定義的公理語(yǔ)義及函數(shù)規(guī)范
    3.6 函數(shù)調(diào)用的公理語(yǔ)義
    3.7 有關(guān)公理
4 翻譯 C程序成時(shí)間邏輯公式的過程
    4.1 詞法分析
    4.2 語(yǔ)法分析
        4.2.1 語(yǔ)法分析技術(shù)
        4.2.2 語(yǔ)法分析的實(shí)現(xiàn)
        4.2.3 BISON輸出程序的分析
    4.3 語(yǔ)義分析
        4.3.1 語(yǔ)義分析概述
        4.3.2 語(yǔ)義分析實(shí)現(xiàn)
    4.4 符號(hào)表
5 基于時(shí)間邏輯的程序驗(yàn)證
    5.1 一般原理
    5.2 驗(yàn)證實(shí)例
    5.3 證明模式
結(jié)論
參考文獻(xiàn)
攻讀碩士學(xué)位期間發(fā)表學(xué)術(shù)論文情況
致謝



本文編號(hào)：3832866