矩阵分块乘法（归纳谓词）
整型矩阵分块相乘。矩阵分块大小可变，但要求能整除矩阵的行、列数。 （验证时间约 387sec）
部分谓词定义采用归纳谓词而不使用全称量化，以避免全称量化的约束区间出现非线性表达式。
[Back to Index]
验证特点：量化断言，宏定义
标注说明：函数前条件：对于矩阵乘 Z = X • Y，宏定义给出了分块大小 b 的限制，和矩阵 X、Y 各元素的取值范围；
函数后条件：Z = X • Y。
程序样例 
