scopelogic工具研究進(jìn)展-文庫吧
2024-09-22 15:03 本頁面
【正文】 這兩個公式已證明，且依賴于原來的 p – 在某分支之后的公式 P被拷貝到 ? 另外一 個分支之后，待證明 ? if語句之后，已經(jīng)證明，依賴于兩個分支之后的 P 傳播證明（ if） ASSERT0( a0 amp。amp。 b0。 ) while (a0 amp。amp。 b0) { ASSERT2( P： a0 amp。amp。 b0 ) if(ab) ASSERT3( ) a = a – (b/a)*a。 ASSERT4( ) else ASSERT5( ) b = b – (a/b)*b。 ASSERT6( ) ASSERT7( ) } ASSERT7( ) a0 amp。amp。 b0 //依賴于 P@2) a0 amp。amp。 b0 //依賴于 P@2 gcd(a,b)==gcd(a@0,b@0) //待證明 gcd(a,b)==gcd(a@0,b@0) //依賴于 P’@4和 P’@6 P’： gcd(a,b)==gcd(a@0,b@0) 傳播（ while） ? while語句 – 如果 P在 while語句之前、以及循環(huán)體之后成立， 那么
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1