矩阵乘法
Zlxn = XlxmxYmxn，其中 Z[i][j] == X[i][1] * Y[1][j] + X[i][2] * Y[2][j] + ... + X[i][m] * Y[m][j]。（验证时间约 8sec）
[Back to Index]
验证特点：自定义谓词，逻辑函数，量化断言，循环变式
标注说明：函数前条件：限定矩阵 X，Y 的大小和元素的取值范围；
函数后条件：Z = X • Y，其中 Z 的每个元素 Z[i][j] == X[i][0..m-1] • Y[0..m-1][j]。
程序样例 
