求最大公约数
求最大公约数的欧几里德算法的验证。 （验证时间约 46sec）
本例有三个函数：（1）欧几里得的“辗转相除法”（递归），和
（2）扩展的欧几里得算法（递归）。在计算a和b的最大公约数gcd的同时求得整数ta和tb，使得 gcd = a*ta + b*tb。
（3）扩展的欧几里得算法（迭代）。同上。
[Back to Index]
验证特点： 逻辑函数，循环变式，中间结果算术溢出的考虑
标注说明： （1）函数1返回值为x和y的最大公约数。（2）函数2在返回x和y的最大公约数gcd的同时，求得整数px和py，使得 gcd = x*px + y*py 成立。
程序样例 
