推斷操做符，映射和量詞

推斷操做符

在VCC中，==>符號意味着邏輯推理結果，即離散數學中的蘊涵關係。P==>Q等價於(（!P）||(Q))。是很是經常使用的操做符。

 

量詞(quantifier)

關於量詞，這裏指的是全稱量詞(universal quantifier)和存在量詞(existential quantifier)。

在VCC中全稱量詞的描述方法是 \forall  T v;E ，意思是「對於任意的T類型的v，表達式E均爲真。

例如：

_(assert x > 1 && \forall int i; 1 < i && i < x ==> x % i != 0)

斷言檢驗x是一個素數。

_(assert \forall int i; \forall int j; 0 <= i && i <= j && j < N ==> b[i] <= b[j])

斷言數組b有序。

 

類似的，在VCC中存在量詞的表達形式是 \exists T v; E，意思是」存在T類型的v，使得表達式E成立「。

例如：

_(assert \exists int i; 0 <= i && i < N && b[i] == 0)

斷言數組b包含元素0。

 

映射(map)

VCC提供映射類型，使用方式有點像數組，可是他們的值不必定是一個簡單的數或者字符，他是兩種類型的數據之間的一種映射關係。如 \integer x [int]是一個從 int類型映射到\integer類型的映射，x[-5]就是在x中-5對應的\integer值，可是因爲沒有給出映射方式，誰也不知道-5映射到哪個\integer上。

注：\integer 表示數學意義上的整數，而\natural則是天然數

關於映射的建立，通常使用lambda表達式。如 \lambda T x;E，表達式將返回一個從T類型的x映射映射到 」x經過表達式E計算以後的結果「，若是表達式E的計算結果類型爲S，那麼這個映射的類型就是S[T]。

例：

_(ghost int av[\natural] = \lambda \natural i;buf[i])

忽略前面的ghost，之後再說，後面的表達式將建立一個av映射，從天然數映射到int類型，映射方式爲buf[i]。