二分查找（引理）
二分查找要求被检索的数组是有序的。 但是有序数组的一些直观性质（数组元素的递增性或递减性）定理证明器直接证明比较困难，需要通过增加引理来增强的能力，以满足任意长度数组的验证。（验证时间约 30sec）
[Back to Index]
验证特点：量化断言，引理
标注说明：函数前条件：作为二分查找的基础，数组具有有序性；
函数后条件：分二种情况表述，即（1）没有找到，返回值=-1。（2）找到，返回值=数组元素的下标。
程序样例 
二分查找要求被检索的数组是有序的。 但是有序数组的一些直观性质（数组元素的递增性或递减性）定理证明器直接证明比较困难，需要通过增加引理来增强的能力，以满足任意长度数组的验证。（验证时间约 30sec）
验证特点：量化断言，引理
标注说明：函数前条件：作为二分查找的基础，数组具有有序性；
函数后条件：分二种情况表述，即（1）没有找到，返回值=-1。（2）找到，返回值=数组元素的下标。
程序样例