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

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

【學位級別】：碩士

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



本文編號：3832866