ホーアロジック、事前条件を計算

Question

if x < 15: 
    x = x+1 
else: 
    x = 0 

事後条件は、Q = {0 < = X < = 15}

れる正しい事前条件P1 = {-1 < = Xを}またはP2 = { 0 < = x < = 15}

どうすれば計算できますか？

Answer 1

どちらもコードフラグメントとポストコンディションの有効な前提条件であるため、弱いもの（この場合はP1）を選択します。 （P2はxの値のより狭い範囲を指定し、これらの値はすべてP1で指定された範囲内にあります）