删除数组元素
查找数组中第一个与给定值x相等的数组元素。若找到则删除该元素，并将数组中其后的所有元素向前移动一位，返回删除元素的数组下标。若找不到，则返回-1。（验证时间约4sec）
[Back to Index]
验证特点：幽灵数组，逻辑变量，assigns子句，量化断言
标注说明：函数前条件：用一个幽灵数组保存实参数组在函数入口处的值，并用逻辑变量记录实参数组的长度；
函数后条件：分二种情况表述，即
1）没有找到要删除的元素，返回值=-1，数组元素的值没有改变。
2）找到，返回值=找到元素的数组下标；该元素被删除，其前的元素没有变化，其后的所有元素都前移了一位。
程序样例 
