标签：
推断操作符
在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]。
标签：
原文地址：http://www.cnblogs.com/aureate-sunshine/p/5020262.html
