關於Assertion

這篇博客開始介紹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驗證他的時候可能就會恍然大悟，這個條件也是要成立的啊！