Логика Хора, расчет предварительного условия

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

условие публикации: Q = {0 ‹= x ‹= 15}

является правильным предварительным условием P1 = {-1 ‹= x} или P2 = {0 ‹= x ‹= 15}

И как я могу его рассчитать?


conditional-statements hoare-logic preconditions
person A. Ano    schedule 02.08.2017    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Оба являются допустимыми предусловиями для фрагмента кода и постусловия, поэтому вы хотите выбрать более слабое, в данном случае это P1. (P2 задает более узкий диапазон значений для x, все из которых присутствуют в диапазоне, указанном P1.)

person Bill the Lizard    schedule 02.08.2017