Hoare Logic, рассчитать предварительное условие

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.)