GCD Example [Yu&Shao'04] Thread1: Thread2: while(a<>b){ while(a<>b){ if(a b) if(b a) a :a-b b b-a; ] } A1=(a=a)∧(a≥b→b=b)∧(GcD(a,b)=GCD(a',b)) G1=(b=b)∧(a≤b→a=a)∧(GCD(a,b)=GCD(a',b) A2三G1( G2=A1 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens GCD Example [Yu&Shao’04] Thread1: while(a<>b){ if(a > b) a := a-b; } Thread2: while(a<>b){ if(b > a) b := b-a; }