VCC簡介與安裝

　　最近在學校跟着老師參與了一個代碼驗證的工做，須要使用Microsoft Research（微軟學術）開發的VCC工具，是開源的，託管在Codeplex上。這東西英語資料極其少，中文資料基本沒有。我只能看官方給的英文文檔。所以，我也就有了心思寫幾篇簡單的博客，也包括文檔的一些翻譯。留個記念也好。

　　VCC主頁（https://vcc.codeplex.com/）

　　

　　翻譯了一下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以前請先在機器上準備好如下的環境：

1. .Net v4.0 or later - Download installer.
2. F# 2.0 Redistributable - Download installer.
3. Microsoft Visual C++ 2010 Redistributable Package - Download installer.
4. Visual Studio 2010 以上(any edition with C++ support). 注意，Express速成版是不推薦的，它不支持在IDE上使用VCC。 我是在Windows10+VS2010上使用的，成功裝上了插件。

 　　

準備好以上的環境以後，你就能夠前往VCC主頁（http://vcc.codeplex.com/）下載最新的安裝程序進行安裝了。