二进制乘法
通过将整型变量 x、y 转化为二进制数的形式来逐位计算乘法 c = x*y 。（验证时间约26sec）
[Back to Index]
验证特点：循环不变式，数值计算中对范围的控制
标注说明：函数前条件：给出 x、y 和 x*y 的范围；
函数后条件：计算结果为 x*y 。
程序样例 
通过将整型变量 x、y 转化为二进制数的形式来逐位计算乘法 c = x*y 。（验证时间约26sec）
验证特点：循环不变式，数值计算中对范围的控制
标注说明：函数前条件：给出 x、y 和 x*y 的范围；
函数后条件：计算结果为 x*y 。
程序样例