八皇后问题（迭代算法）
八皇后问题是指在 8×8 格的国际象棋上摆放八个皇后，使其不能互相攻击，即任意两个皇后都不能处于同一行、同一列或同一斜线上。
该问题是回溯算法的典型案例，通过遍历所有方案求得全部的解法。本例是八皇后问题的迭代求解算法。 （验证时间约 138sec）
[Back to Index]
验证特点：量化断言，幽灵变量，归纳谓词
标注说明：函数 EightQueens 利用全局数组记录一个解的状态，并且找到一个，输出一个。函数没有形参和返回值，所以函数协议的前后条件均为\true。
程序样例 
