NASA的10條代碼編寫原則

NASA的10條代碼編寫原則

做者: Gerard J. Holzmann 來源: InfoQ
原文連接 git

英文原文:NASA’s 10 Coding Rules for Writing Safety Critical Program程序員

譯/ 大愚若智github

image
image

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

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

  在普通人的眼中,NASA是一個很「高級」的機構,其成員包含大量不一樣領域的科學家和研究人員。與其餘任何組織機構相似,NASA的平常工做,以及所執行的幾乎所有項目也離不開計算機的輔助,出於需求的特殊性和重要性,他們所使用的不少計算機軟件都是內部自行開發的,在一些重要項目的關鍵領域發揮着做用。app

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

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

  大型的複雜軟件項目一般會遵循必定的代碼編寫標準和指南。這些指南奠基了軟件開發過程當中必須遵照的基本原則。工具

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

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

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

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

  緣由在於這種語言具有完善的工具支持,包括邏輯模型分離器、調試器、靜態編譯器、強源(Strong source)代碼分析器,以及度量工具等。

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

原則1 – 簡化控制流程(Simple Control Flow)

  使用盡量精簡的控制流程構造編寫程序 —— 不要使用setjmplongjmp構造、goto語句,以及直接或間接的recursion

  緣由:簡化控制流程有助於提升代碼清晰度,加強代碼可驗證能力。不使用遞歸,便不會產生循環的函數調用圖,這樣也可證實全部本應有界的執行實際上都是有界的。

原則2 – 爲循環使用固定次數上限(Fixed Upper Bound for Loops)

  全部循環必須有固定次數的上限。咱們能夠經過驗證工具靜態地證實,爲循環中迭代數量所設立的上限次數未被超越。

  若是沒法以靜態方式對循環的次數界限加以證實,則可認爲未遵照該原則。

  緣由:爲循環設置次數界限,避免使用遞歸,這些作法有助於預防代碼失控。然而該原則沒法適用於本就不該終止的迭代(例如進程調度器)。此時將沿用該原則的逆向原則:必須可以靜態地證實迭代不能終止。

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

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

  緣由:諸如malloc等內存分配機制,以及垃圾回收器一般會產生沒法預知的行爲,進而可能會對性能產生影響。更重要的是,還有可能由於程序員的失誤形成內存錯誤,例如:

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

  應強制全部模塊位於固定大小、預先分配的存儲區域中,藉此可避免此類問題,並簡化內存使用狀況的驗證工做。

  堆中未分配內存的狀況下,動態請求內存的惟一方式是使用棧內存。

原則4 – 不使用冗長的函數(No Large Functions)

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

  緣由:過長的函數一般意味着結構並不是最優。每一個函數都應是可理解且可驗證的單一邏輯單位。若是在計算機顯示器上須要多屏界面才能完整顯示,這樣的邏輯單位一般會極難理解。

原則5 – 低斷言密度(Low Assertion Density)

image
image

  程序的斷言密度(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語句的返回值也應進行檢查。

  緣由:若是對一個錯誤結果的響應與對成功結果的響應本不該有任何區別,那麼很明顯須要檢查返回值。一般對closeprintf的調用便符合這種狀況。此時一種可行的方法是將函數的返回值明確拋出給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對這些原則的見解

  這些原則就如同汽車安全帶,也許一開始會以爲有些不溫馨,但很快會變成每一個人的第二本能,到時候很難想象會有人不這麼作。

相關文章
相關標籤/搜索