[發明專利]一種計算機語言轉換系統及C語言到MSVL語言的轉換方法

有效

• 申請號: 201310120182.1
• 申請日: 2013-04-08
• 公開（公告）號: CN103150200A
• 公開（公告）日: 2013-06-12
• 發明（設計）人: 段振華;于妍;田聰;王小兵;張南;韓萌
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F9/45
• 分類號: G06F9/45
• 代理公司: 北京科億知識產權代理事務所(普通合伙) 11350
• 代理人: 湯東鳳

技術領域

本發明涉及計算機程序設計語言C語言技術領域，尤其涉及一種C語言結構化語句到MSVL對應語句的轉換方法。

背景技術

C語言是一種通用的、過程式的編程語言，廣泛用于系統與應用軟件的開發。具有高效、靈活、功能豐富、表達力強和較高的移植性等特點，在程序員中備受青睞。2011ISO正式公布的C語言新的國際標準草案C11，提高了對C++的兼容性，并將新的特性增加到C語言中。新功能包括支持多線程，基于ISO/IEC?TR19769:2004規范下支持Unicode，提供更多用于查詢浮點數類型特性的宏定義和靜態聲明功能。雖然C語言廣泛適用于各類系統與軟件的開發，但是保證其正確性和安全性成為一個巨大的挑戰。模型檢測是驗證系統正確性的一個有效手段，但要抽取C語言程序的抽象模型成為目前面對的一個難點和挑戰。

時序邏輯作為一種系統建模與驗證工具已廣泛應用于軟件工程、數字電路設計等領域。投影時序邏輯（PTL）對ITL進行了擴展，時序邏輯語言MSVL是PTL的一個可執行子集，是一個集建模（Modeling）、仿真（Simulation）和驗證（Verification）為一體的時序邏輯程序設計語言，它將系統的建模與性質的描述統一于同一邏輯框架內，通過模型檢測技術驗證系統的性質。投影時序邏輯在實時和混合系統，特別是安全危急系統的形式描述和驗證方面也是極其有用的，例如，載人航天系統是一個復雜的混合實時系統，為了保證系統的安全性和可靠性，傳統的測試方法遠遠不能滿足要求，采用形式化的驗證技術是十分有用的。

另外，投影時序邏輯程序設計語言MSVL的語言結構和C語言極其類似，很容易產生對應的轉換關系。通過實現從C語言向MSVL語言的轉化，對轉化后的目標程序進行驗證，利用等價轉化的思想，可以實現對C語言形式化模型的抽取，并且可以對該模型進行模型檢測，這將大大提高C語言程序的安全性和可靠性。

發明內容

本發明提供一種計算機語言轉換系統，其能將C語言轉換成MSVL語言，以對C語言的程序進行檢測。其具體包括，一種計算機語言轉換系統，其用于將C語言程序轉換成MSVL語言程序，其特征在于：其包括，

詞法分析模塊，其將字符序列轉換為單詞序列，所述字符序列包括C語言中的關鍵字、標識符、常數、運算符、頭文件以及注釋行的定義；

語法分析模塊，其基于yacc中所規定的C語言的相關詞法規則，進而識別出C語言中特定的語句；

轉換處理模塊，其根據C語言與MSVL語言之間的語言轉換規律將C語言轉換成MSVL語言。

本發明還提供一種C語言到MSVL語言的轉換方法，其提供詞法分析模塊、語法分析模塊及轉換處理模塊，其特征在于：所述方法包括以下步驟；

第一步：將C語言程序導入詞法分析模塊，該步驟包括將字符序列轉換為單詞序列，所述字符序列包括C語言中的關鍵字、標識符、常數、運算符、頭文件以及注釋行的定義；

第二步：將步驟一中得到的單詞流導入語法分析模塊，該步驟包括基于yacc中所規定的C語言的相關詞法規則，進而識別出C語言中特定的語句；

第三步：將第二步語法分析識別出的C語言語句序列在轉換處理模塊中根據相應的轉換規則轉換成對應的MSVL語句；

第四步：用時序操作符“；”連接得到的MSVL語句序列，得到MSVL程序。

在上述技術方案的基礎上，語法分析模塊中所述的C語言中的結構化語句包括基本表達式語句、while語句、if語句、if-else語句、for語句、switch語句、printf語句以及scanf語句。

在上述技術方案的基礎上，所述語法分析模塊中所述的C語言中結構化語句的while語句、for語句的循環體和if語句、if-else語句的條件語句是一個語句塊。

在上述技術方案的基礎上，所述C語言與MSVL語言之間的語言轉換規律包括表達式轉換規則、語句轉換規則和語句塊轉換規則。。

在上述技術方案的基礎上，所述表達式的轉化規則如下：

對表達式進行轉化，假設x和y是標準符號，e代表一個常量或變量，參照規則如下：

如果表達式為e，則轉化為MSVL表達式返回e;

如果表達式為[x++|x--],則轉化為MSVL語句x:=x+1and?skip或者x:=x-1and?skip;

如果表達式為x=y,則轉化為MSVL語句x:=y?and?skip;

如果表達式為x==y,則轉化為MSVL語句x==y;