最近在學校跟著老師參與了一個代碼驗證的工作，需要使用Microsoft Research（微軟學術）開發的VCC工具，是開源的，托管在Codeplex上。這東西英語資料極其少，中文資料基本沒有。我只能看官方給的英文文檔。因此，我也就有了心思寫幾篇簡單的博客，也包括文檔的一些翻譯。留個紀念也好。
翻譯了一下VCC教程上的簡介：
“VCC是一個驗證環境，用與驗證c語言編寫的程序。VCC獲取一個程序(注釋了功能, 斷言和類型不變量)並試圖證明那些注釋是正確的,也就是說,他們對每一個可能的程序執行。環境包括工具監測證明嘗試和構建部分反例執行失敗的證明。VCC處理細粒度並發性和低級的C語言特性,並已用於驗證成千上萬行商業並發系統的代碼的功能正確性。本教程描述如何使用VCC驗證C代碼。它涵蓋了注釋語言、驗證方法和使用VCC本身。
本教程介紹如何使用VCC驗證C代碼。我們的主要受眾是的想編寫正確的代碼的C程序員。唯一的要求是擁有C語言的工作知識。使用VCC，你首先要注釋你的代碼，指明他做什麼(如：為你的輸入進行排序)，以及為什麼它能這樣做(如：與你的循環和數據結構相適應的不變量）。然後VCC會試圖(以數學的方式)證明程序符合你之前訂下的規范。與大多數程序分析器不同，VCC不會尋找bug，或者分析程序的抽象；如果VCC證明程序是正確的，那麼您的程序是就是正確的。
為了檢查程序，VCC使用演繹驗證模式。它生成一定數量的數學表達式(稱為驗證條件)，保證程序的正確性的“有效性表達式(?)”，並試圖使用一個自動定理驗證器來證明這些語句。如果這些證明失敗，VCC會將失敗的原因反映到你的程序代碼身上（而不是讓你看到定理驗證器用的那些公式）。因此，你通常是在代碼和程序狀態層面與VCC交互的。通常情況下，你可以忽略在VCC內部的數學推理。例如，如果您的程序使用了除法，如果VCC無法證明除數一定非零，它會報告你的程序有(潛在的)錯誤。這並不意味著你的程序必然是不正確的。事實上，大多數情況下它都沒有問題。（VCC會報錯）那是因為你還沒有提供足夠的信息來讓VCC推斷出這個疑似錯誤一定不會發生。(例如，你可能沒有指定一個函數參數是必須非零)。通常，你會通過加強你的注釋來解決這個“錯誤”。不過這可能又會導致其他的錯誤報告，迫使你添加更多的注釋。所以實際的驗證是一個迭代的過程。有時，這個過程將揭示一個真正的編程錯誤。但即使它沒有，你至少也能會證明你的代碼不受這種錯誤影響，同時你也會產生精確的規格注釋——一種非常有用的文檔。
本教程涵蓋了VCC注釋語言的基礎。當你弄懂了這篇教程，你應該就能夠使用VCC來驗證一些重要的項目了。這篇教程不包括VCC的理論背景，實現細節和高級主題。你可以從VCC主頁上可以找到這些信息。教程中的所有小結的更多信息都可以VCC手冊中找到。本教程中的示例和VCC源碼在一起。
你可以通過命令行或者Visual Studio 2008/2010使用VCC（譯者：更新的版本也沒關系）。Visual Studio 提供接口讓你方便地訪問VCC工具鏈的不同的組件，因而一般推薦使用它。VCC可以從VCC主頁（http://vcc.codeplex.com/）下載，一定要閱讀安裝說明，裡面提供了關於安裝條件和設置工具路徑的方法等重要信息。”
安裝
安裝VCC之前請先在機器上准備好以下的環境：
准備好以上的環境之後，你就可以前往VCC主頁（http://vcc.codeplex.com/）下載最新的安裝程序進行安裝了。
