Assumption

接下來是第二種註釋語句類型Assumption。語法_(Assume E), 這個表達式是讓VCC在接下來的額推理中，無視表達式E, 直接承認表達式E。

例：

int x, y;

_(assume x != 0)

y = 100 / x;

在沒有那條assumption以前，VCC確定不會經過驗證，由於x可能爲0。可是，加了Assumption以後，VCC就選擇放棄治療，將x!=0加入本身的資料庫。可是你用assumption糊弄了VCC並無什麼好處，由於當代碼實際運行的時候，沒有人會管那堆註釋，當X剛好爲0的時候，程序就要crash了。因此通常來講，若是你但願你的驗證可靠的話，Assumption就只能是驗證過程當中臨時性的產物，最終仍是儘可能消除的。

聽起來assumption不是個好東西，其實否則，他也是有很多做用的。

1.當你代碼比較複雜，VCC難以驗證的時候，你能夠用assumption先跳過，assumption也是一個標記，往後再去驗證他。

2.當你調試那些註釋的時候，你能夠用assumption縮小錯誤範圍，幫助定位錯誤。

3.對於複雜的程序，VCC驗證須要很長的時間，使用assumption可讓VCC放棄治療，快速經過那段代碼，提升你編寫調試註釋的效率。

4.可使用assumption模擬程序運行環境。

甚至VCC本身驗證程序的時候，也在背地裏使用assumption。

int x;

_(assert x == 1)

_(assert x > 0)

好比在上面的例子中，第一個assertion會報錯，可是第二個不會。由於VCC給第一個Assertion報錯以後，爲了繼續找到更多的錯誤，他就寫了一個_(assume x==1）。

例：

int x,y;

_(assert x > 5)

_(assert x > 3)

_(assert x < 2)

_(assert y < 3)

結果

_(assert x > 5) // fails

_(assert x > 3) // succeeds

_(assert x < 2) // fails

_(assert y < 3) // fails