<<
>>

Проверка требований к инварианту I 1.

Поскольку

2. Очевидно, что I не зависит от у х, которое является условием продолжения цикла.

3.

Далее, должна обеспечиваться истинность В нашем примере

имеем

Применяя аксиому присваивания к у :: получим {у + 1 {у = х}. Таким образом, и это доказано.

5. В заключение надо решить вопрос о завершении нашего цикла

Учитывая, что х и у — целые числа, легко видеть: цикл завершается за конечное число шагов. Этот шаг завершает доказательство корректности полученного инварианта.

Если выполнение 5-го требования (завершение цикла) не гарантируется, то описание цикла называют частично корректным, в противном случае — полностью корректным.

<< | >>

Еще по теме Проверка требований к инварианту I 1.:

  1. II. 1. 4. Инварианты.
  2. Проверка содержательности и достоверности информации является более сложным делом и требует другого аппарата и других методов проверки.
  3. § 24 Замена одного требования другим противоположным (компенсация). – Основания сей замены и законные для нее условия. – Однородность требований. – Отношение их по количеству. – Действие несостоятельности на замену. – Требования несоизмеримые. – Необязательность замены.
  4. 4. Кондикционное требование и требование стороны в обязательстве о возврате исполненного
  5. 2. Кондикционное требование и требование о возврате исполненного по недействительной сделке
  6. § 5. Соотношение кондикционного требования с обязательствами возврата, а также с требованиями, составляющими содержание договорной ответственности (п. 2483—2485)
  7. Статья 162. Аудиторская проверка
  8. 12.5. Тактика проверки показаний на месте
  9. § 10. Психология проверки показаний на месте
  10. ПРОВЕРКА ГИПОТЕЗ СТАТИСТИЧЕСКИХ
  11. Проверка показаний на месте
  12. Проверка криминалистической версии
  13. Правило критической проверки веера версий.
  14. 6.2.6. Шаг пятый :проверка причинности
  15. Статья 687. Проверка соблюдения продавцом условий договора купли-продажи
  16. Проверка версий о самооговоре