基于模板元編程的量綱檢測方法
量綱誤用在科學(xué)計算程序中是一種常見(jiàn)的錯誤,然而程序設計語(yǔ)言的標準類(lèi)型系統卻對此無(wú)能為力。物理方程中的量綱錯誤可以手工分析出來(lái),然而求解物理方程的計算機程序中的量綱錯誤卻難以被發(fā)現,因為計算程序往往很復雜。例如,一些研究者認為火星氣候探測衛星的丟失,是因為程序中把一個(gè)英制單位的變量傳遞給了使用公制單位的模塊。因而,量綱的正確性對計算結果的正確性非常重要。
本文引用地址:http://dyxdggzs.com/article/201706/347825.htm近年來(lái),研究者們提出了一些量綱檢測方法,典型的如Osprey量綱檢測方法。Osprey方法包含5個(gè)主要步驟:
(1)對待檢測源程序進(jìn)行單位標注,使得檢測器能夠知道每個(gè)變量的單位;
(2)C語(yǔ)言解析和語(yǔ)法檢查;
(3)生成包含單位信息的抽象語(yǔ)法樹(shù);
(4)生成約束CY程);
(5)方程的化簡(jiǎn)及高斯消去求解(GE)。
可以看出,Osprey方法步驟較多,每步都需要語(yǔ)言外的其他工具,并需要對其進(jìn)行修改、擴充,而且最后的高斯消去(GE)計算量非常大,是Osprey方法的性能瓶頸。使用Osprey方法還有一個(gè)問(wèn)題,就是需要同時(shí)維護2份源代碼:一份正常代碼用于編譯測試;另一份包含量綱信息的檢測代碼,修改正常代碼后必須及時(shí)對檢測代碼進(jìn)行更新,維護起來(lái)也比較繁瑣。此外,由于C++語(yǔ)言的解析非常困難,Osprey方法目前沒(méi)有實(shí)現對C++程序的量綱檢測。
針對這些問(wèn)題,提出一種基于模板元編程的量綱檢測方法TADA(TMP-bAsed Dimensional AnalysisMethod),其基本思路是利用程序設計語(yǔ)言自身的模板元編程(Template Meta Programming,TMP)功能,讓編譯器在編譯時(shí)對程序中的量綱進(jìn)行準確性檢測,從而可以避免Osprey方法的計算量大等諸多問(wèn)題。TADA方法具有下列優(yōu)點(diǎn):
(1)TADA方法可使得應用開(kāi)發(fā)人員不需要維護2份代碼,因為使用TADA方法的檢測程序也完全是一個(gè)合法的可編譯的程序。
(2)TADA方法的量綱檢測完全在編譯期間進(jìn)行,對程序不會(huì )引入任何運行時(shí)開(kāi)銷(xiāo)。
(3)TADA方法無(wú)需進(jìn)行方程組求解工作,可以適用于任何規模的程序。與Osprey等方法類(lèi)似,TADA方法也需要手工對程序添加量綱信息,其標注的工作量與Osprey等方法相當。但TADA方法中編譯器在進(jìn)行檢測的時(shí)候無(wú)需進(jìn)行Osprey方法中的方程組求解工作,因而不再有Osprey方法的計算瓶頸。
(4)TADA方法采用模塊化設計,使得單位的表示與匹配檢測之間實(shí)現了松耦合,支持用戶(hù)可以以一致的方式增加新的單位。
1 模板元編程(TMP)技術(shù)
在C++程序設計語(yǔ)言中,模板元編程是實(shí)現代碼重用的一種重要機制。下面首先對模板元編程技術(shù)進(jìn)行介紹,然后給出TADA方法中需要使用的幾個(gè)基本的模板元程序。
1.1 模板元編程簡(jiǎn)介
模板可以將類(lèi)型定義為參數,以提高代碼的可重用性。模板包括類(lèi)模板和函數模板等。函數模板與模板函數的區別可以類(lèi)比于類(lèi)與對象的區別:函數模板是模板的定義;而模板函數是函數模板的實(shí)例,具有程序代碼,占用內存空間。當編譯系統發(fā)現了函數模板一個(gè)對應的函數調用后,根據實(shí)參的類(lèi)型來(lái)確認是否匹配函數模板中對應的形參,然后生成一個(gè)重載函數,稱(chēng)該重載函數為模板函數。類(lèi)似地,在聲明了一個(gè)類(lèi)模板后,也可以創(chuàng )建類(lèi)模板的實(shí)例一模板類(lèi)。
類(lèi)模板的一般形式如下:
template
class類(lèi)名{
//類(lèi)定義…
};
C++模板系統能夠通過(guò)模板的特化、偏特化實(shí)現邏輯判斷,并能通過(guò)模板遞歸實(shí)現循環(huán),構成了一個(gè)圖靈完全的二級語(yǔ)言。使用這種二級語(yǔ)言進(jìn)行編程叫作C++模板元編程(Template Meta Programming,TMP)。模板元編程的驅動(dòng)力是模板的遞歸實(shí)例化。
下面給出C++模板元編程的一個(gè)示例。
首先定義一個(gè)類(lèi)模板,通過(guò)該類(lèi)模板可實(shí)現在編譯期間計算4的任意次方。如下所示:
通過(guò)下面的程序來(lái)使用該模板。
程序Test.cpp執行完后,會(huì )正確輸出4的7次方的值,該數值是C++編譯器在編譯模板元程序時(shí)遞歸計算得到。由于模板元程序完全在編譯期間執行,相當于對編譯器功能進(jìn)行擴充,因而利用這種程序進(jìn)行量綱檢測具有良好的可行性。
1.2 基本模板元程序
下面給出TADA方法中需要使用的幾個(gè)基本的模板元程序。
(1)靜態(tài)判斷

語(yǔ)法:StaticlF::ResultType
語(yǔ)義:當cond為真時(shí),ResuhType為T(mén)1,否則ResuhType為T(mén)2。
(2)靜態(tài)斷言

語(yǔ)義:當cond為真時(shí)什么也不做,否則產(chǎn)生一個(gè)編譯期錯誤(UnitError沒(méi)有定義,或void函數不應該有返回值)。
(3)靜態(tài)絕對值


語(yǔ)義:遞歸的使用輾轉相除法在編譯期間求出a與b的最大公約數,其中a與b為int類(lèi)型。
2 TADA量綱檢測方法
TADA量綱檢測方法需要涉及到單位和量綱的表示、計算、標注以及數學(xué)運算函數的量綱包裝等各個(gè)組成步驟,下面將依次對其進(jìn)行介紹。
2.1 單位和量綱的表示
在Osprey方法中,量綱是用一個(gè)長(cháng)度為7的向量表示的,每個(gè)分量對應一個(gè)SI標準量綱。TADA方法中也采用了這種方式。為了簡(jiǎn)化闡述,本文只討論長(cháng)度、重量、時(shí)間這三種量綱,其SI單位分別為米、千克和秒(TADA方法可直接推廣到其他各種量綱)。由于TMP程序的特殊性,它并沒(méi)有數組或向量的支持,也不能使用浮點(diǎn)數據(使用浮點(diǎn)數表示量綱也會(huì )帶來(lái)不精確性),量綱在TMP程序中的表示形式有所不同:用u11,u12,u21,u22,u31,u32之類(lèi)的整型量分別表示

,

并輔以ratio表示同量綱、不同單位之間的比值,如分鐘和秒的比值為60。
TADA方法可靜態(tài)地建立如下常用單位:


模板元程序在計算公式的時(shí)候需要推導出新的量綱,例如在計算

的時(shí)候,編譯器應該能根據等號右邊的公式計算出它的量綱,并與e的量綱進(jìn)行比較判別。TADA方法的量綱是用分數形式表示的,在每次量綱計算之后都需要進(jìn)行分數的約分處理,才能進(jìn)行相等性判斷,因而TADA方法可用如下的方式處理新生成單位,如下所示。

2.2 單位和量綱的計算
由于量綱都是用分數表示的,因而其計算會(huì )稍有麻煩。下面定義TADA方法中量綱分數的加、減、乘、除和等價(jià)測試運算。
(1)分數的加法運算,如下所示。

(2)分數的減法運算。TADA方法通過(guò)加法實(shí)現減法計算,如下所示。

語(yǔ)義:分數相減并約分,即:

(3)單位相乘。分別將3個(gè)量綱分數相加,然后使用BuildUnit生成新單位。

語(yǔ)義:?jiǎn)挝籙a與單位Ub相乘后的新單位。
(4)單位相除。與乘法處理方式相似。

語(yǔ)義:若單位ua與單位Ub等價(jià)則不產(chǎn)生任何效果,否則產(chǎn)生編譯期錯誤。
2.3 單位和量綱標注的原理和語(yǔ)法
與Osprey等方法類(lèi)似,TADA方法也在待檢測源程序進(jìn)行單位標注,以使得檢測器能夠知道每個(gè)變量的單位。由于經(jīng)過(guò)單位標注的待檢測程序仍然是合法的可編譯的程序,所以標注信息必須由語(yǔ)言自身已有的語(yǔ)法要素構成;標注信息還不能影響被標注變量的任何計算特性及使用方式,只有滿(mǎn)足這兩點(diǎn)要求的標注方式才能使標注工作量最小化。此外,已標注變量應該禁止從未標注變量進(jìn)行各種隱含的類(lèi)型轉換,這樣嚴格的限制才能有效進(jìn)行單位量綱的匹配檢測。對于C++語(yǔ)言來(lái)說(shuō),可以采用模板類(lèi)的方式實(shí)現。
標注實(shí)質(zhì)上是把語(yǔ)言原始的數據類(lèi)型替換成TADA方法預定義的模板類(lèi),而模板類(lèi)實(shí)現了各種運算符號的重載,同時(shí)禁止了任何隱含的類(lèi)型轉換,使得量綱標注既滿(mǎn)足語(yǔ)法要素的要求,又滿(mǎn)足計算兼容性的要求和禁止隱含轉換的要求。TADA方法中標注的實(shí)現如下所示。


2.4 定義單位量綱
量綱檢測系統應該預定義常用單位量綱,以方便應用開(kāi)發(fā)人員使用。TADA方法采用如下方式定義單位量綱:


2.5 數學(xué)運算函數的量綱包裝
對于指數、對數、三角函數等已有的數學(xué)運算函數,其參數與返回值都是沒(méi)有單位量綱的,不能直接用于有量綱的公式計算。針對這個(gè)問(wèn)題,.TADA方法提供了這些函數的量綱包裝,以sqrt和sin為例如下:

2.6 輔助工具
TADA方法還提供了一些輔助工具,用于將量綱變量以適合閱讀的方式顯示出來(lái),例如:

可以得到這樣的輸出結果:0.2米/秒2
2.7 分析和評估
在TADA方法的基礎上,實(shí)現了面向C/C++程序的量綱檢測系統(TADA系統),并對TADA系統的檢測能力進(jìn)行了分析和評估。
首先采用TADA系統來(lái)檢測下面的樣例程序。

在TADA系統中,Visual Studio 2003編譯該程序會(huì )出現類(lèi)似如下的錯誤信息,錯誤信息的第3行就表明了unit.epp的第9行有錯誤。

在檢測能力方面,采用文獻的樣例程序對TA-DA系統和Osprey系統的量綱檢測能力進(jìn)行了對比評估。在文獻中,Osprey共找到了3個(gè)錯誤,其中前2個(gè)是單位誤用錯誤,第3個(gè)是單位轉換比例因子錯誤。TADA系統也完全找到了前2個(gè)錯誤,而第3個(gè)錯誤在標注時(shí)被避免掉了,因為該單位系統包含了量綱之間的比例因子,能夠進(jìn)行自動(dòng)的單位轉換。
在性能和可擴展性方面,TADA系統能夠更有效地實(shí)現對c/c++程序的量綱檢測。Osprey系統引入了具有較高計算復雜度的線(xiàn)性方程組求解步驟,需要很大的計算和時(shí)間開(kāi)銷(xiāo)來(lái)解線(xiàn)性解方程組。TADA系統基于模板元編程技術(shù),只需要利用語(yǔ)言自身的語(yǔ)法能力,靠編譯器進(jìn)行單位量綱檢查,沒(méi)有帶來(lái)太多額外的復雜計算。并且TADA系統不會(huì )帶來(lái)任何程序的運行時(shí)開(kāi)銷(xiāo)。因此TADA系統可適用于各種規模的C/C++程序,具有更好的性能和可擴展性。
在易用性方面,TADA系統的標注負擔與Osprey系統相當。由于TADA系統利用C++編譯器的功能進(jìn)行錯誤檢測,而C++編譯器遇到模板錯誤時(shí)的錯誤信息卻不很直觀(guān),錯誤報告的可讀性較弱,但仍可以快速定位到錯誤點(diǎn)。
3 結 語(yǔ)
這里提出一種新穎的基于模板元編程的單位量綱檢測方法TADA,并基于該方法實(shí)現了一個(gè)單位量綱檢測系統。
TADA方法采用模板元編程技術(shù),使得經(jīng)過(guò)單位量綱標注的受測程序仍然是一個(gè)完整、合法、可編譯的C/C++程序,無(wú)需維護多套程序代碼,也無(wú)需進(jìn)行復雜的解方程組運算,就能夠在程序代碼中發(fā)現量綱錯誤,具有良好的實(shí)用性和可擴展性,可以有效適用于多種規模程序的量綱檢測。
評論