Метод счетчиков

Идея этого метода состоит во введении в программу Prgm новых переменных-счетчиков, добавляемых по одной в каждый цикл программы. Переменная-счетчик должна инициализироваться перед входом в цикли увеличивать свое значение при каждом прохождении по циклу.

В преобразованной таким образом программе Prgm’ измененные инварианты циклов представляются в виде, содержащем условие ограниченности значений счетчиков функциями, зависящими только от входных переменных.

В отличие от метода Флойда этот метод не требует введения ограничивающих функций в контрольных точках. Переменные-счетчики рассматриваются как органическая часть программы, позволяющая логически выразить свойство завершенности в инвариантах цикла.

Преимущество этого метода перед методом Флойда состоит в том, что одни и те же инварианты используются при доказательстве частичной корректности и завершенности. Однако метод Флойда обладает большей общностью.

Успех доказательства завершенности в методе счетчиков определяется тем, удастся ли подобрать соответствующее условие ограниченности счетчика в инварианте цикла.

Этот метод, так же как и метод Флойда, требует творческого подхода программиста.

Лекция 10. Тестирование программных продуктов