矩阵分块乘法（宏定义）
矩阵分块大小可变，但要求能整除矩阵的行、列数。为描述整除的性质需要引入引理。（验证时间约 460sec）
在多重循环的情况下，内层循环的循环不变式需要保留外层循环的一些性质，使用宏定义可以使标注简化。
[Back to Index]
验证特点：宏定义，自定义谓词，逻辑函数，量化断言，逻辑宏定义，引理，幽灵语句，多重循环
标注说明：函数前条件：对于矩阵乘 Z = X • Y，宏定义给出了分块大小 的限制，和矩阵 X、Y 各元素的取值范围
函数后条件：Z = X • Y。
程序样例 
