魔方问题
魔方问题是指生成一个 n*n 的矩阵，使每个单元取 1 到 n*n 的一个整数值，各单元的取值互不相重，并要求每行、每列、以及两条主对角线的和都相等。
本例是一个生成算法的验证（算法及程序实现参见《Fundamentals of Data Structures in C》一书）。 （验证时间约 60sec）
[Back to Index]
验证特点： 自定义谓词，存在量词
标注说明： 函数协议描述魔方的生成算法：从第一行中间的元素填1，a[0][(n-1)/2] = 1，开始，将数字 1～n*n 依次向矩阵的左上单元填写，如果左上单元已有数字，则向下方单元填写，直至所有的数字填入a的相应单元中。
程序样例 
