scopelogic工具研究進展(編輯修改稿)
2024-11-17 15:03 本頁面
【文章內(nèi)容簡介】 P在 循環(huán)體之后，以及循環(huán)之后都成立 – P實際上 是循環(huán)不變式 ? while語句之前的公式被復制到 – 循環(huán)體之后，待證明 – 循環(huán)體之前以及 while語句之后，依賴于語句之前的公式和語句之后的 公式 ? 僅 當確認 P是循環(huán)不變式時才可以傳播 傳播（ while） ASSERT0( P： a0 amp。amp。 b0。 ) while (a0 amp。amp。 b0) { ASSERT2( ) if(ab) ASSERT3( ) a = a – (b/a)*a。 ASSERT4( ) else ASSERT5( ) b = b – (a/b)*b。 ASSERT6( ) ASSERT7( ) } ASSERT7( ) P： a=0 amp。amp。 b=0 //依賴于 P@0和 P@7 P： a=0 amp。amp。 b=0 //待證明 P
教學課件相關推薦
鄂ICP備17016276號-1