羅京麗 杜建革
摘 要:量綱誤用是科學計算應用程序中一種常見的錯誤,對計算結果的正確性影響很大。在此提出一種基于模板元編程的量綱檢測方法TADA,能夠有效完成C和C++程序代碼的量綱檢測工作。該方法利用程序設計語言自身的模板元編程功能,通過定義相關的量綱模板及其計算和標注方法,依靠編譯器在編譯期間完成量綱分析和檢測,無需任何運行開銷,有效解決了傳統量綱檢測系統中解方程組的計算量瓶頸等問題。
關鍵詞:模板元編程;TADA;量綱;計算量瓶頸
中圖分類號:TP393 文獻標識碼:B 文章編號:1004-373X(2009)04-080-06
Dimensional Unit Analysis Method Based on Template Meta-programming
LUO Jingli1,DU Jiange2
(1.Jiangxi Light Industry College,Yichun,336000,China;2.Nanjing University of Technology,Nanjing,210094,China)
Abstract:Misuse of measurement units is a common mistake in many scientific computing applications.It greatly influences the correctness of the application results.TADA,a tool that effectively detects errors of this kind for C/C++ programs is proposed.Making use of the function of template meta-programming in the language itself,TADA analyses the dimensional units and detects mismatches only by a standard C++ compiler in compile time without any runtime overhead.It avoids the computational bottleneck of solving linear equations introduced by traditional methods.
Keywords:template meta-programming;TADA;measurement unit;computational bottleneck
0 引 言
量綱誤用在科學計算程序中是一種常見的錯誤,然而程序設計語言的標準類型系統卻對此無
能為力。物理方程中的量綱錯誤可以手工分析出來,然而求解物理方程的計算機程序中的量綱錯誤卻難以被發現,因為計算程序往往很復雜。例如,一些研究者認為火星氣候探測衛星的丟失,是因為程序中把一個英制單位的變量傳遞給了使用公制單位的模塊[1]。因而,量綱的正確性對計算結果的正確性非常重要。
近年來,研究者們提出了一些量綱檢測方法[2-5],典型的如Osprey量綱檢測方法[2]。Osprey方法包含5個主要步驟:
(1) 對待檢測源程序進行單位標注,使得檢測器能夠知道每個變量的單位;
(2) C語言解析和語法檢查;
(3) 生成包含單位信息的抽象語法樹;
(4) 生成約束(方程);
(5) 方程的化簡及高斯消去求解(GE)。
可以看出,Osprey方法步驟較多,每步都需要語言外的其他工具,并需要對其進行修改、擴充,而且最后的高斯消去(GE)計算量非常大,是Osprey方法的性能瓶頸。使用Osprey方法還有一個問題,就是需要同時維護2份源代碼:一份正常代碼用于編譯測試;另一份包含量綱信息的檢測代碼,修改正常代碼后必須及時對檢測代碼進行更新,維護起來也比較繁瑣。此外,由于C++語言的解析非常困難,Osprey方法目前沒有實現對C++程序的量綱檢測。
針對這些問題,提出一種基于模板元編程的量綱檢測方法TADA(TMP-bAsed Dimensional Analysis Method),其基本思路是利用程序設計語言自身的模板元編程(Template Meta Programming,TMP)功能,讓編譯器在編譯時對程序中的量綱進行準確性檢測,從而可以避免Osprey方法的計算量大等諸多問題。TADA方法具有下列優點:
(1) TADA方法可使得應用開發人員不需要維護2份代碼,因為使用TADA方法的檢測程序也完全是一個合法的可編譯的程序。
(2) TADA方法的量綱檢測完全在編譯期間進行,對程序不會引入任何運行時開銷。
(3) TADA方法無需進行方程組求解工作,可以適用于任何規模的程序。與Osprey等方法類似,TADA方法也需要手工對程序添加量綱信息,其標注的工作量與Osprey等方法相當。但TADA方法中編譯器在進行檢測的時候無需進行Osprey方法中的方程組求解工作,因而不再有Osprey方法的計算瓶頸。
(4) TADA方法采用模塊化設計,使得單位的表示與匹配檢測之間實現了松耦合,支持用戶可以以一致的方式增加新的單位。
1 模板元編程(TMP)技術
在C++程序設計語言中,模板元編程[6-8]是實現代碼重用的一種重要機制。下面首先對模板元編程技術進行介紹,然后給出TADA方法中需要使用的幾個基本的模板元程序。
1.1 模板元編程簡介
模板可以將類型定義為參數,以提高代碼的可重用性。模板包括類模板和函數模板等。函數模板與模板函數的區別可以類比于類與對象的區別:函數模板是模板的定義;而模板函數是函數模板的實例,具有程序代碼,占用內存空間。當編譯系統發現了函數模板一個對應的函數調用后,根據實參的類型來確認是否匹配函數模板中對應的形參,然后生成一個重載函數,稱該重載函數為模板函數。類似地,在聲明了一個類模板后,也可以創建類模板的實例—模板類。
類模板的一般形式如下:
template
class 類名{
//類定義…
};
C++的模板系統能夠通過模板的特化、偏特化實現邏輯判斷,并能通過模板遞歸實現循環,構成了一個圖靈完全的二級語言[6]。使用這種二級語言進行編程叫作C++模板元編程(Template Meta Programming,TMP)。模板元編程的驅動力是模板的遞歸實例化。下面給出C++模板元編程的一個示例。
首先定義一個類模板,通過該類模板可實現在編譯期間計算4的任意次方。如下所示:
pow4.hpp
#ifndef POW4_HPP
#define POW4_HPP
//primary template to compute;
template
class Pow4 {
public:
enum { result = 4 * Pow4
};
//full specialization to end the recursion
template<>
class Pow4<0> {
public:
enum { result = 1 };
};
通過下面的程序來使用該模板。
Test.cpp
#endif // POW4_HPP
#include
#include "pow4.hpp"
int main()
{
std::cout << "Pow4<7>::result = "
<< Pow4<7>::result << '\n';
}
程序Test.cpp執行完后,會正確輸出4的7次方的值,該數值是C++編譯器在編譯模板元程序時遞歸計算得到。由于模板元程序完全在編譯期間執行,相當于對編譯器功能進行擴充,因而利用這種程序進行量綱檢測具有良好的可行性。
1.2 基本模板元程序
下面給出TADA方法中需要使用的幾個基本的模板元程序。
(1) 靜態判斷
template
struct StaticIF
{
typedef T2 ResultType;
};
template
struct StaticIF
{
typedef T1 ResultType;
};
語法:StaticIF
語義:當cond為真時,ResultType為T1,否則ResultType為T2。
(2) 靜態斷言
template
template<> void StaticAssert
語法:StaticAssert
語義:當cond為真時什么也不做,否則產生一個編譯期錯誤(UnitError沒有定義,或void函數不應該有返回值)。
(3) 靜態絕對值
template
struct StaticABS
{
static const int value = n>=0 ? n :-n;
};
語法:StaticABS
語義:n的絕對值,其中n為int類型。
(4) 靜態最大公約數
template
struct StaticGCD
{ //b!=0
static const int result = StaticIF<(a,StaticGCD >::ResultType::result;
};
template
{
static const int result=a;
};
語法:StaticGCD::result
語義:遞歸的使用輾轉相除法在編譯期間求出a與b的最大公約數,其中a與b為int類型。
2 TADA量綱檢測方法
TADA量綱檢測方法需要涉及到單位和量綱的表示、計算、標注以及數學運算函數的量綱包裝等各個組成步驟,下面將依次對其進行介紹。
2.1 單位和量綱的表示
在Osprey方法中,量綱是用一個長度為7的向量表示的,每個分量對應一個SI標準量綱。TADA方法中也采用了這種方式。為了簡化闡述,本文只討論長度、重量、時間這三種量綱,其SI單位分別為米、千克和秒(TADA方法可直接推廣到其他各種量綱)。由于TMP程序的特殊性,它并沒有數組或向量的支持,也不能使用浮點數據(使用浮點數表示量綱也會帶來不精確性),量綱在TMP程序中的表示形式有所不同:用u11,u12,u21,u22,u31,u32之類的整型量分別表示米u11u12,千克u11u12,秒u11u12,并輔以ratio表示同量綱、不同單位之間的比值,如分鐘和秒的比值為60。
TADA方法可靜態地建立如下常用單位:
Struct UnitRoot//無量綱
{
static const int u11 = 0;
static const int u12 = 1;
static const int u21 = 0;
static const int u22 = 1;
static const int u31 = 0;
static const int u32 = 1;
static const double ratio;
};
const double UnitRoot::ratio=1;
struct ULength: UnitRoot {}; //長度量綱
struct UWeight: UnitRoot {}; //重量量綱
struct UTime:UnitRoot {}; //時間量綱
struct UAngle:UnitRoot {}; //角的大?。o量綱)
struct UnitLess :UnitRoot {}; //無量綱
struct UMeter:ULength{static const int u11=1;}; //米
struct UKG:UWeight{static const int u21=1;}; //千克
struct USecond:UTime{static const int u31=1;}; //秒
struct UAcceleration:UnitRoot {static const int u11=1;//加速度:米/秒^2
static const int u31=-2;};
struct URadian: UAngle{}; //角度
struct UAngleDegree:UAngle{static const double ratio;}; //弧度
const double UAngleDegree::ratio=180/3.141592653589793;
//弧度與角度的比例
模板元程序在計算公式的時候需要推導出新的量綱,例如在計算“e=12mv2”的時候,編譯器應該能根據等號右邊的公式計算出它的量綱,并與e的量綱進行比較判別。TADA方法的量綱是用分數形式表示的,在每次量綱計算之后都需要進行分數的約分處理,才能進行相等性判斷,因而TADA方法可用如下的方式處理新生成單位,如下所示。
template
struct BuildUnit :public UnitRoot
{
static const int gcd1 = StaticGCD
static const int gcd2 = StaticGCD
static const int gcd3 = StaticGCD
static const int u11 = U11/gcd1;
static const int u12 = U12/gcd1;
static const int u21 = U21/gcd2;
static const int u22 = U22/gcd2;
static const int u31 = U31/gcd3;
static const int u32 = U32/gcd3;
};
2.2 單位和量綱的計算
由于量綱都是用分數表示的,因而其計算會稍有麻煩。下面定義TADA方法中量綱分數的加、減、乘、除和等價測試運算。
(1) 分數的加法運算,如下所示。
template
struct FractionAdd
{
static const int U1=u11*u22+u21*u12;
static const int U2=u12*u22;
};
語法:FractionAdd
語義:分數相加并約分,即:
U1U2=u11*u22+u21*u12u12*u22,且GCD(U1,U2)=1。
(2) 分數的減法運算。
TADA方法通過加法實現減法計算,如下所示。
template
struct FractionSub
{
static const int U1=FractionAdd
static const int U2=FractionAdd
};
語法:FractionSub
語義:分數相減并約分,即:
U1U2=u11*u22-u21*u12u12*u22,且GCD(U1,U2)=1。
(3) 單位相乘。
分別將3個量綱分數相加,然后使用BuildUnit生成新單位。
template
struct UnitMultiply
{
typedef FractionAdd b::u12> FM1; typedef FractionAdd b::u22> FM2; typedef FractionAdd b::u32> FM3; typedef BuildUnit< FM1::U1,FM1::U2, FM2::U1,FM2::U2, FM3::U1,FM3::U2> ResultType; }; 語法:UnitMultiply 語義:單位Ua與單位Ub相乘后的新單位。 (4) 單位相除。 與乘法處理方式相似。 template struct UnitDivide { typedef FractionSub b::u12> FM1; typedef FractionSub b::u22> FM2; typedef FractionSub b::u32> FM3; typedef BuildUnit< FM1::U1,FM1::U2, FM2::U1,FM2::U2, FM3::U1,FM3::U2> ResultType; }; 語法:UnitDivide 語義:單位Ua除以單位Ub后的新單位。 (5) 單位的等價測試函數(宏) #define UNIT_CHECK(a,b) StaticAssert< (a::u11==b::u11) && (a::u12==b::u12) && (a::u21==b::u21) && (a::u22==b::u22) && (a::u31==b::u31) && (a::u32==b::u32)>() 語法:UNIT_CHECK(Ua,Ub); 語義:若單位Ua與單位Ub等價則不產生任何效果,否則產生編譯期錯誤。 2.3 單位和量綱標注的原理和語法 與Osprey等方法類似,TADA方法也在待檢測源程序進行單位標注,以使得檢測器能夠知道每個變量的單位。由于經過單位標注的待檢測程序仍然是合法的可編譯的程序,所以標注信息必須由語言自身已有的語法要素構成;標注信息還不能影響被標注變量的任何計算特性及使用方式,只有滿足這兩點要求的標注方式才能使標注工作量最小化。此外,已標注變量應該禁止從未標注變量進行各種隱含的類型轉換,這樣嚴格的限制才能有效進行單位量綱的匹配檢測。對于C++語言來說,可以采用模板類的方式實現。 標注實質上是把語言原始的數據類型替換成TADA方法預定義的模板類,而模板類實現了各種運算符號的重載,同時禁止了任何隱含的類型轉換,使得量綱標注既滿足語法要素的要求,又滿足計算兼容性的要求和禁止隱含轉換的要求。TADA方法中標注的實現如下所示。 template //T為基礎變量類型(int、double...) struct UnitBase//U為單位量綱信息 { typedef UnitBase T value; //實際的數值 UnitBase(){} explicit //禁止從基礎類型進行隱含構造轉換 UnitBase(T init_value):value(init_value){} operator T (){return value;} //允許向基礎類型隱含轉換 //以下定義各種運算符,使得標注類可以模擬原始變量進行各種運算 #define TEMPLATE template TEMPLATE UnitBase(const UnitBase { UNIT_CHECK(U,U2);//單位等價性檢測 value=rhs.value; } TEMPLATE ThisType& operator = (UnitBase { UNIT_CHECK(U,U2); value=rhs.value; return *this; } TEMPLATE bool operator == (UnitBase
{
UNIT_CHECK(U,U2);
return value==rhs.value;
}
TEMPLATE ThisType& operator += (UnitBase
{
UNIT_CHECK(U,U2);
value+=rhs.value;
return *this
}
TEMPLATE ThisType& operator -= (UnitBase
{
UNIT_CHECK(U,U2);
value-=rhs.value;
return *this
}
TEMPLATE ThisType operator + (UnitBase
{
UNIT_CHECK(U,U2);
return ThisType(value+rhs.value);
}
TEMPLATE ThisType operator - (UnitBase
{
UNIT_CHECK(U,U2);
return ThisType(value-rhs.value);
}
TEMPLATE UnitBase
operator * (UnitBase
{
typedef UnitMultiply::ResultType TT;
return UnitBase
}
TEMPLATE ThisType& operator *= (UnitBase
{
UNIT_CHECK(U2,UnitRoot);
value*=rhs.value;
return *this;
}
TEMPLATE UnitBase
operator / (UnitBase
{
typedef UnitDivide::ResultType TT;
return UnitBase
}
#undef TEMPLATE
//以下定義可以顯式禁止其他一切引起隱含類型轉換的運算
template
template
template
template
template
template
template
(T2 rhs){return UnitError;}
template
};
2.4 定義單位量綱
量綱檢測系統應該預定義常用單位量綱,以方便應用開發人員使用。TADA方法采用如下方式定義單位量綱:
{//米
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
namespace KG //千克
{
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
namespace Second//秒
{
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
namespace Acceleration //加速度:米/秒^2
{
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
namespace Radian//弧度
{
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
namespace AngleDegree //角度
{
typedef UnitBase
typedef UnitBase
typedef UnitBase
typedef UnitBase
}
……
2.5 數學運算函數的量綱包裝
對于指數、對數、三角函數等已有的數學運算函數,其參數與返回值都是沒有單位量綱的,不能直接用于有量綱的公式計算。針對這個問題,TADA方法提供了這些函數的量綱包裝,以sqrt和sin為例如下:
#define HALF_UNIT(U) BuildUnit
template
UnitBase U> n) {//開方函數應使單位的所有量綱減半 return UnitBase } #undef HALF_UNIT template UnitBase {//正弦函數的參數應為弧度,返回值為無量綱 UNIT_CHECK(U,URadian); return UnitBase } 2.6 輔助工具 TADA方法還提供了一些輔助工具,用于將量綱變量以適合閱讀的方式顯示出來,例如: Unit::Second::Double n(10); Unit::Meter::Double m(20); cout< 可以得到這樣的輸出結果: 0.2米/秒^2 2.7 分析和評估 在TADA方法的基礎上,實現了面向C/C++程序的量綱檢測系統(TADA系統),并對TADA系統的檢測能力進行了分析和評估。 首先采用TADA系統來檢測下面的樣例程序。 unit.cpp #include "unit.h" using namespace std; int main(int argc,char* argv[]) { Unit::Second::Double n(10); Unit::Meter::Double m(20); Unit::KG::Double c; //示量綱不匹配 c=m/n/n; return 0; } 在TADA系統中,Visual Studio 2003編譯該程序會出現類似如下的錯誤信息,錯誤信息的第3行就表明了unit.cpp的第9行有錯誤。 meta_prog_basic.h(15) :error C2065:"UnitError":未聲明的標識符 d:\My Documents\Visual Studio Projects\unit\unit_core.h(70) :參見…的引用 d:\My Documents\Visual Studio Projects\unit\unit.cpp(9) :參見…的引用 … 在檢測能力方面,采用文獻[2]的樣例程序對TADA系統和Osprey系統的量綱檢測能力進行了對比評估。在文獻[2]中,Osprey共找到了3個錯誤,其中前2個是單位誤用錯誤,第3個是單位轉換比例因子錯誤。TADA系統也完全找到了前2個錯誤,而第3個錯誤在標注時被避免掉了,因為該單位系統包含了量綱之間的比例因子,能夠進行自動的單位轉換。 在性能和可擴展性方面,TADA系統能夠更有效地實現對C/C++程序的量綱檢測。Osprey系統引入了具有較高計算復雜度的線性方程組求解步驟,需要很大的計算和時間開銷來解線性解方程組。TADA系統基于模板元編程技術,只需要利用語言自身的語法能力,靠編譯器進行單位量綱檢查,沒有帶來太多額外的復雜計算。并且TADA系統不會帶來任何程序的運行時開銷。因此TADA系統可適用于各種規模的C/C++程序,具有更好的性能和可擴展性。 在易用性方面,TADA系統的標注負擔與Osprey系統相當。由于TADA系統利用C++編譯器的功能進行錯誤檢測,而C++編譯器遇到模板錯誤時的錯誤信息卻不很直觀,錯誤報告的可讀性較弱,但仍可以快速定位到錯誤點。 3 結 語 這里提出一種新穎的基于模板元編程的單位量綱檢測方法TADA,并基于該方法實現了一個單位量綱檢測系統。 TADA方法采用模板元編程技術,使得經過單位量綱標注的受測程序仍然是一個完整、合法、可編譯的C/C++程序,無需維護多套程序代碼,也無需進行復雜的解方程組運算,就能夠在程序代碼中發現量綱錯誤,具有良好的實用性和可擴展性,可以有效適用于多種規模程序的量綱檢測。 參 考 文 獻 [1]Mars Climate Orbiter Mishap Investigation.ftp://ftp.hq.nasa.gov/pub/pao/reports/1999/MCO_report.pdf. [2]Jiang Lingxiao,Su Zhendong.Osprey:A Practical Type System for Validating Dimensional Unit Correctness of C Programs.Proc.of ICSE′06.Shanghai,2006. [3]Allen E E,Hase D,V.Luchangco,et al.Object-oriented Units of Measurement.Proc.of OOPSLA′04.Canada,2004:384-403. [4]Brown W E.Applied Template Meta-programming in SIUNITS:The Library of Unit-based Computation.http://www.oonumerics.org/tmpwol/brown.pdf,2001. [5]Foster J S,Ahndrich M F,Aiken A.A Theory of Type Qualifiers.Proc.of PLDI′99.Ottawa,1999,34(5):192-203. [6]Todd L Veldhuizen.C++ Templates are Turing-complete.http://osl.iu.edu/~tveldhui/papers/2003/turing.pdf. [7]Micolai Josuttis,David Vandevoorde.C++ Templates:The Complete Guide.Pearson Education,2003. [8]The Boost:MPL Library.http://www.boost.org. [9]Anderson E,Bai Z,Bischof C,et al.LAPACK Users′ Guide.Third Edition.Society for Industrial and Applied Mathematics,1999. [10]Das M,Lerner S,Seigle M.ESP:Path-sensitive Program Verification in Polynomial Time.Proc.of PLDI′02.Ottawa,2002:57-68. [11]Antoniu T,Steckler R A,Krishnamurthi S,et al.Validating the UnitCorrectness of Spread Sheet Programs.Proc.of ICSE′04.Edinburg,2004:439-448. 作者簡介 羅京麗 女,1977年出生,江西安福人,江西省輕工高級技校講師,學士。主要研究方向為計算機軟件和計算機應用。 杜建革 男,1973年出生,重慶人,南京理工大學碩士。主要研究領域為計算機軟件和計算機應用。 注:本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。