這篇博客開始介紹VCC的用法，先用簡單的例子介紹VCC的基本語法，當然面對更復雜的程序時，VCC也是將他簡化然後分析的。
1.Assertion
#include <vcc.h>
int main() {
int x,y,z;
if (x <= y) z = x;
else z = y;
_(assert z <= x)
return 0;
}
上面的代碼使z成為x和y之中的最小值。其中被_( )包圍的注釋就是VCC所需要的注釋，而且C語言編譯器會無視這些注釋。因為include的<vcc.h>中定義了#define _(...) /∗nothing∗/
一個類似_(assert E)的注釋就是一個Assertion，他要求VCC證明注釋中的表達式E是成立（hold）。所以_(assert z <= x)要求當代碼執行到這一行時，z應該小於等於x。需要注意的是，如果VCC驗證通過了這一條Assertion，這表示VCC證明不管什麼時候，不管執行多少次，這條Assertion都會成立。
C語言自身也有類似的東西 assert(E)。微軟的文檔中這樣介紹兩者的區別。
It is instructive to compare_(assert E)with the macro assert(E) (defined in <assert.h>), which evaluates E at runtime and aborts execution if E doesn’t hold. First, assert(E) requires runtime overhead (at least in builds where the check is made), whereas_(assert E)doesnot.Second,assert(E)will catch failure of the assertion only when it actually fails in an execution, whereas _(assert E) is guaranteed to catch the failure if it is possible in any execution. Third, because _(assert E) is not actually executed, E can include unimplementable mathematical operations, such as quantification over infinite domains.
如果要在cmd命令行中用VCC驗證這個函數，你可以把代碼保存為minimum.c，在命令行中使用VCC大致如下，**表示代碼文件目錄。
C:\**> vcc.exe minimum.c
Verification of main succeeded.
如果裝了VCC的Visual Studio插件，用VS打開文件之後，空白處右擊，在菜單中選擇Verify minimum.c就可以驗證這個文件，驗證結果會在VS底部給出。如果在函數內點擊也可以只驗證這個函數。
2.VCC的原理部分
要理解VCC的工作原理，可以去了解每一步執行中VCC掌握了什麼信息。在上面的例子中VCC一開始什麼都不知道，然後知道了if的第一個條件x<=y, 然後是z==x, 所以VCC知道z<=x。在else分支中，類似的，VCC知道y<x, z==y, 所以VCC知道z<=x。if的每個分支VCC都發現Assertion成立，最後他就會驗證通過這個Assertion。
我們說VCC知道什麼，指的是VCC知道代碼提供的信息，並且可以通過當前已知的信息可以直接推斷出新的信息。在這種理想狀態下，當你新增一個正確的Assertion，肯定不會影響他後面的Assertion的正確性。但是，VCC只完成了對基本公式的繼續推斷，包括相等，不等，加減乘除等簡單的運算，而沒有完成對所有運算公式的自動推斷，是有其局限性的。不然的話，他自己全部都能推斷完，我們的工作量就很小了。
所以，在現實情況中，有時候，即使VCC“知道”了足夠的信息，也沒法證明一條Assertion。當你新增一個正確的Assertion，有可能會影響他後面的Assertion的正確性。當然，這個概率是比較低的，而且往往是涉及非線性算法的代碼會出問題。
所以，VCC驗證順序代碼或者條件語句時一般不會丟失信息，但是VCC驗證循環語句的時候，容易丟失信息。這裡的丟失是指他沒有繼續推斷出更多信息，提供注釋有助於減少這種情況。如果VCC沒有通過你認為肯定能通過驗證的代碼，那就有可能是VCC不知道或者忽視了你以為它肯定知道的東西。這時候一個Assertion也是一個提醒，VCC驗證他的時候可能就會恍然大悟，這個條件也是要成立的啊！
