二分查找
二分查找要求被检索的数组是有序的。 （验证时间约 65sec）
函数从数组段a[0..len-1]的区间开始，每次确认该区间的中间值并与要查找的值val进行比较：
（1）若相等，查找成功返回此数组下标；
（2）若不相等，根据数组的有序性将当前查找区间缩小一半，确认新的查找区间。查找不到时返回-1。
[Back to Index]
验证特点：量化断言
标注说明：函数前条件：给出数组有序性的描述；
函数后条件：分二种情况表述，即（1）没有找到，返回值=-1。（2）找到，返回值=数组元素的下标。
程序样例 
