霍尔逻辑，计算前置条件

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 指定的范围内。