NASA的10條代碼編寫原則

作者: Gerard J. Holzmann 來源: InfoQ
原文鏈接

英文原文：NASA’s 10 Coding Rules for Writing Safety Critical Program

譯/ 大愚若智

本文將介紹由 NASA 噴氣推進實驗室首席科學家 Gerard J. Holzmann 所提出的，側重於安全參數的10條代碼編寫原則

　　美國宇航局（National Aeronautics and Space Administration，縮寫為 NASA） 是美國聯邦政府的一個獨立機構，負責制定、實施美國的民用太空計劃、與開展航空科學暨太空科學的研究。在太空計劃之外，美國國家航空航天局還進行長期的民用以及軍用航空航天研究。

　　在普通人的眼中，NASA是一個很“高級”的機構，其成員包含大量不同領域的科學家和研究人員。與其他任何組織機構類似，NASA的日常工作，以及所執行的幾乎全部項目也離不開計算機的輔助，出於需求的特殊性和重要性，他們所使用的很多計算機軟件都是內部自行開發的，在一些重要項目的關鍵領域發揮著作用。

　　去年，一位前NASA實習生把美國阿波羅登月項目的11號計算機 --- 阿波羅導航計算機 (Apollo Guidance Computer) 系統源代碼上傳到了 GitHub，此舉在開發者群體中引起了極大的熱議。

　　此外，NASA官方也已將自己的部分源代碼開源到 GitHub，讓我們得以管窺這一頂尖科研機構內的聰明大腦們寫代碼的專業水平。

　　大型的復雜軟件項目通常會遵循一定的代碼編寫標準和指南。這些指南奠定了軟件開發過程中必須遵守的基本原則。

a) 代碼的結構如何安排？
b) 應當或不應當使用哪些語言特性？

　　出於效果的角度考慮，這些原則必須盡可能精簡並且必須足夠具體，這樣才能更好地被人理解並記憶。

　　本文將介紹由 NASA 噴氣推進實驗室首席科學家 Gerard J. Holzmann 所提出的，側重於安全參數的10條代碼編寫原則。當然，這些原則也適用於其他編程語言。

　　為 NASA 工作的全球頂尖程序員在編寫高度安全的代碼時就沿襲了這樣的一套指南。實際上，很多組織，包括NASA噴氣推進實驗室主要會選擇使用C語言編寫代碼。

　　原因在於這種語言具備完善的工具支持，包括邏輯模型分離器、調試器、靜態編譯器、強源（Strong source）代碼分析器，以及度量工具等。

　　有時候，編寫代碼必須遵守一定的原則，尤其是在代碼的正確性會對人的生命產生決定性影響的領域，例如飛機、將宇航員送上同步軌道的航天器，以及距離居住地僅幾英裏遠的核電站等設施運行的控制代碼。

原則1 – 簡化控制流程（Simple Control Flow）

　　使用盡可能精簡的控制流程構造編寫程序 —— 不要使用setjmp或longjmp構造、goto語句，以及直接或間接的recursion。

　　原因：簡化控制流程有助於提高代碼清晰度，增強代碼可驗證能力。不使用遞歸，便不會產生循環的函數調用圖，這樣也可證明所有本應有界的執行實際上都是有界的。

原則2 – 為循環使用固定次數上限（Fixed Upper Bound for Loops）

　　所有循環必須有固定次數的上限。我們可以通過驗證工具靜態地證明，為循環中叠代數量所設立的上限次數未被超越。

　　如果無法以靜態方式對循環的次數界限加以證明，則可認為未遵守該原則。

　　原因：為循環設置次數界限，避免使用遞歸，這些做法有助於預防代碼失控。然而該原則無法適用於本就不應終止的叠代（例如進程調度器）。此時將沿用該原則的逆向原則：必須能夠靜態地證明叠代不能終止。

原則3 – 不使用動態內存分配（No Dynamic Memory Allocation）

　　不要在初始化完成後進行動態內存分配。

　　原因：諸如malloc等內存分配機制，以及垃圾回收器通常會產生無法預知的行為，進而可能會對性能產生影響。更重要的是，還有可能因為程序員的失誤造成內存錯誤，例如：

• 試圖分配超過可用物理內存數的內存
• 忘記釋放內存
• 繼續使用已被釋放的內存
• 對已分配內存進行越界使用

　　應強制所有模塊位於固定大小、預先分配的存儲區域中，借此可避免此類問題，並簡化內存使用情況的驗證工作。

　　堆中未分配內存的情況下，動態請求內存的唯一方式是使用棧內存。

原則4 – 不使用冗長的函數（No Large Functions）

　　任何函數的長度不應超過使用標準參考格式（每個聲明最多一行，每個語句最多一行）打印的紙張上一頁紙所能容納的字符數。這意味著函數的代碼不應超過60行。

　　原因：過長的函數通常意味著結構並非最優。每個函數都應是可理解且可驗證的單一邏輯單位。如果在計算機顯示器上需要多屏界面才能完整顯示，這樣的邏輯單位通常會極難理解。

原則5 – 低斷言密度（Low Assertion Density）

　　程序的斷言密度（Assertion density）應平均保持為每個函數最少兩個斷言。斷言可用於檢查現實運行過程中本絕不應出現的異常狀況，因此應定義為Boolean測試。當斷言失敗後，應執行明確的恢復操作。

　　如果靜態檢查工具證明斷言絕對不會Fail或Hold，則可認為未遵守該原則。

　　原因：業界的代碼編寫工作統計報告顯示，通過單元測試可發現，通常我們所編寫的每10-100行代碼中至少會存在一處缺陷。隨著斷言密度的增高，攔截缺陷的機會也會增大。

　　斷言的另一個重要之處在於，它是防禦性編程（Defensive coding）策略的重要組成部分。我們可以使用斷言驗證函數執行前後的狀況，函數的執行參數和返回值，以及循環不變式（Loop-invariant）。在完成性能關鍵代碼的測試工作後，可將斷言選擇性地禁用。

原則6 – 以最小範圍級別聲明數據對象（Declare Data Objects at Smallest Level of Scope）

　　該原則同時也是數據隱蔽（Data hiding）的基本原則。所有數據對象均必須以盡可能最小的範圍級別進行聲明。

　　原因：如果某對象不在範圍內，意味著其值將無法引用或已損壞。該原則不鼓勵出於多種可能導致故障診斷工作變得更復雜的互斥意圖重用變量。

原則7 – 檢查參數和返回值（Check Parameters and Return Value）

　　應在每次調用函數後檢查非空函數的返回值，並應在每個函數內部檢查參數的合法性。

　　在最嚴格的形式下，該原則意味著就算printf語句和文件close語句的返回值也應進行檢查。

　　原因：如果對一個錯誤結果的響應與對成功結果的響應本不應有任何區別，那麽很明顯需要檢查返回值。通常對close和printf的調用便符合這種情況。此時一種可行的方法是將函數的返回值明確拋出給void，這意味著開發者明確（而非意外地）決定忽略該返回值。

原則8 – 限制預處理程序的使用（Limited Use of Preprocessor）

　　預處理程序（Preprocessor）應僅限用於頭文件和宏定義。遞歸的宏調用、令牌傳遞，以及變量參數列表均不允許使用。就算大型應用程序開發工作中，標準樣板文件（Boilerplate）之外也可能有必要使用一兩個以上的條件編譯指令，這是為了避免將同一個頭文件包含多次。每個這種用法必須通過工具檢查器添加標記，並通過代碼闡述原因。

　　原因：C語言預處理程序是一個強大但較為含糊的工具，有可能徹底破壞代碼的清晰度，並讓很多基於文本的檢查器產生混淆。就算具備正式的語言定義，包含無界限預處理程序代碼的構造也會顯得非常難以解讀。

　　有關條件編譯的註意事項同樣很重要 – 就算只使用10個條件編譯指令，代碼也有會產生1024（2^10）個可能的版本，這會導致測試工作量劇增。

原則9 – 限制指針的使用（Limited Use of Pointers）

　　指針的使用必須加以限制。通常只允許不超過一層的解引用（Dereferencing）。指針解引用操作不應隱藏在typedef聲明或宏定義內部。此外函數指針也是不允許使用的。

　原因：指針很容易被濫用，就算專家也難以徹底避免。指針的存在會使得我們難以跟蹤或分析程序中數據的流動，尤其是在使用基於工具的靜態分析器執行這些操作時。函數指針還會對靜態分析器所能執行的檢查類型產生限制，因此除非有非常必要的理由，否則一般不推薦使用。如果使用函數指針，通常幾乎將無法通過工具證明遞歸的缺席，此時只能提供其他方法彌補這種分析能力的缺失。

原則10 – 編譯所有代碼（Compile all Code）

　　從開發工作第一天開始時，就必須對所有代碼進行編譯。必須啟用編譯器的警告功能，並使用最細致的檢查選項。代碼必須能通過這樣的設置在不產生任何警報的情況下順利編譯完成。

　　所有代碼必須每天一次、使用至少一種（多種則更好）最新型的靜態源代碼分析器進行檢查，並且必須順利通過分析器的整個檢查過程而不產生任何警告。

　　原因：市面上有很多效果卓越的源代碼分析器，其中很多甚至是以免費軟件的形式發布的。對於這樣可以直接使用的現成技術，任何軟件開發工作都沒理由不加以充分利用。

　　如果編譯器或靜態分析器遇到問題，導致問題/錯誤的代碼必須重寫，這樣才能進一步改善代碼質量。

NASA對這些原則的看法

　　這些原則就如同汽車安全帶，也許一開始會覺得有些不舒適，但很快會變成每個人的第二本能，到時候很難想象會有人不這麽做。

NASA的10條代碼編寫原則