八皇后问题（递归算法）
八皇后问题是指在 8×8 格的国际象棋上摆放八个皇后，使其不能互相攻击，即任意两个皇后都不能处于同一行、同一列或同一斜线上。
该问题是回溯算法的典型案例，通过遍历所有方案求得全部的解法。本例是八皇后问题的递归求解算法。 （验证时间约 90sec）
[Back to Index]
验证特点：量化断言，存在量词，归纳谓词，递归
标注说明：本例有3个函数：
1）checkq 检查当前皇后k放的位置是否合理，即a[k]是否与a[1..k-1]中的皇后在同一列或同一个对角线。
2）eightQueensRec 从第k位皇后开始递归测试所有8位皇后的放置可能，输出探测中找到的解。如果解的数量超出整型的表示范围，则程序中止退出。
3）main 从 k=1 调用eightQueensRec函数。
程序样例 
