幾類While循環終止性分析的理論、方法及其套用

《幾類While循環終止性分析的理論、方法及其套用》是依託電子科技大學,由李軼擔任醒目負責人的青年科學基金項目。

基本介紹

• 中文名：幾類While循環終止性分析的理論、方法及其套用
• 依託單位：電子科技大學
• 項目類別：青年科學基金項目
• 項目負責人：李軼

項目摘要

正確性是程式的最重要的屬性之一。包含終止性分析的程式驗證被稱為完全的正確性驗證。眾所周知，循環終止性問題的描述和研究由來已久，對其終止性的判定和證明依然無法完全解決。因此，對具普遍意義的基本循環程式模型進行終止性分析將具有十分重要的意義。近年來，計算機代數領域建立的深刻理論及工具已逐漸在計算機視覺，自動控制等領域得到廣泛套用。最近，諸如DISCOVERER和BOTTEMA等實代數工具已逐漸被套用於程式變元為實變數的嵌入式軟體的分析及驗證中。目前，我們已線上性及非線性循環程式終止性分析問題上展開了工作，並取得了初步成果。以計算機代數為理論基礎，結合符號-數值混合計算方法，本項目擬在幾類非線性循環程式的終止性分析，線性循環終止性的離線判定等方面做深入研究，並藉助所建立的理論和已有的實代數工具，對出現於嵌入式軟體中的幾類循環程式進行終止性分析。

結題摘要

本項目套用計算機代數和實代數中的深刻理論及成熟工具，採取符號與數值計算相結合的方法對廣泛存在於實際套用中的幾類線性和非線性循環程式的終止性進行分析和驗證。 我們主要從兩個方面來進行循環程式的終止性分析。其一，從可判定的角度進行終止性分析。儘管程式終止性問題早在上世紀30年代就被Tiwari證明是不可判定的，但人們仍然熱衷於去探尋可判定的子類。其二，採用合成Ranking函式的方式進行終止性分析。基於Ranking函式合成的驗證方法並不是完備的。這是因為，雖然，Ranking函式的存在印證了循環程式是可終止的，但Ranking函式不存在卻並不能說明循環程式是不可終止的。因此，Ranking函式的存在僅僅是循環程式可終止的充分而非必要的條件。儘管如此，基於Ranking函式的終止性驗證方法仍是當今進行終止性分析的主流方法。 首先，從可判定角度，我們對一類線性while循環程式的終止性問題進行了分析。這類循環在2004年首次被斯坦福教授Tiwari提出，並證明了它在實數域上的終止性是可判定的。但是，我們發現，在多數情形下，如果此類循環程式是不可終止的，那么，Tiwari的方法所給出的點是一個N-不可終止點，即這樣的點需要再疊代N次後才能成為一個不可終止點。而在他的文章中也並沒有給出N的計算方法。因此，基於這個發現，我們提出了一種方法去計算N的值。其次，基於賦值矩陣Jordan塊的特殊結構，我們將這類線性循環程式的終止性問題歸於為兩類特殊線性程式的終止性問題。而後者的終止性更易被判定。更為重要的是，如果該類循環程式是不可終止的，那么，我們的新算法能構造至少一個不可終止點。本項目中，除了對上述的線性循環程式的終止性進行分析外，我們也研究了部分非線性循環程式的終止性。一般地，非線性循環程式的終止性因為其更為複雜的疊代動力行為，從而導致其終止性方面的研究甚少。通過分析無窮疊代序列在某些條件下所呈現出的良好性質，我們證明了三類非線性循環程式在實數域上的終止性是可判定的，並證明了其是不可終止的充要條件是疊代函式在循環條件所形成的區域中有不動點。 其次，藉助工具DISCOVERER和CDS理論，我們也建立了基於Ranking函式合成的終止性驗證方法。新方法中，我們引進一些鬆弛變數，從而使得最終的半代數系統更容易讓現有的工具去自動求解。