用戶設計意圖的程式標註及其類型驗證技術研究

《用戶設計意圖的程式標註及其類型驗證技術研究》是依託南京理工大學，由趙洋擔任項目負責人的青年科學基金項目。

基本介紹

• 中文名：用戶設計意圖的程式標註及其類型驗證技術研究
• 項目類別：青年科學基金項目
• 項目負責人：趙洋
• 依託單位：南京理工大學

項目摘要

隨著軟體規模日趨龐大、形態更加複雜，其可信性卻越來越脆弱。傳統的軟體工程方法已經無法滿足當今社會對軟體可靠性和正確性的迫切需求，軟體理論與方法學的研究面臨重要的科學挑戰，其中如何抽象地表述各種用戶需求並與具體的程式代碼相互印證成為構建可信賴軟體的關鍵之一。本項目以面向對象軟體的自動分析與驗證為研究背景，探查用戶的各種設計意圖，分析用於顯式聲明軟體行為特徵和對象數據屬性的常用程式標註及其語義，結合當前許可類型系統中類型規則和形式變換等理論成果，將形式化的許可類型作為橋樑，溝通抽象的程式標註和具體的程式代碼，並進一步驗證兩者間的一致性，實現軟體系統的正確性確認；在此基礎上，設計並實現一個基於許可類型系統的程式分析和驗證的原型系統。本項目旨在探索基於程式語言通用類型系統的形式化驗證技術，為用戶設計意圖的準確勾勒、多程式標註的語義融合、許可類型系統的擴展和今後的工程套用奠定理論和技術基礎。

結題摘要

本項目以面向對象軟體的自動分析與驗證為研究背景，探查用戶的各種設計意圖，分析用於顯式聲明軟體行為特徵和對象數據屬性的常用程式標註及其語義，結合當前許可類型系統中類型規則和形式變換等理論成果，將形式化的許可類型作為橋樑，溝通抽象的程式標註和具體的程式代碼，並進一步驗證兩者間的一致性，實現軟體系統的正確性確認。在面向對象軟體系統中，我們遴選了部分規範化的程式標註，這些標註顯著的特點是能夠歸納並抽象各種對象數據屬性、軟體行為特徵和函式模組接口，顯式聲明用戶的多種設計意圖和軟體屬性。在此基礎上，我們嘗試綜合理解多樣化程式標註之間的內在關聯，並通過形式化的許可類型對其進行語義表述；以基本對象為研究單位，討論對象狀態的分割和保護這一關鍵性的問題，通過探索許可類型系統中的類型規則和形式變換理論，正確定義靜態的許可類型與動態的程式狀態之間的一致性關聯，分別在進展和保持定理的基礎上證明了許可類型系統的安全性。此外，我們還進一步改進了基於傳統數據流的程式分析和驗證算法，以許可類型為媒介驗證程式標註與程式代碼的匹配性，從而溝通抽象用戶設計意圖和具體程式代碼之間的障礙，實現了原型系統的設計並達到了預期的目標。本項目旨在探索基於程式語言通用類型系統的形式化驗證技術，為用戶設計意圖的準確勾勒、多程式標註的語義融合、許可類型系統的擴展和今後的工程套用奠定理論和技術基礎。