Билет 3. Основные управляющие конструкции в Си. Понятие инварианта цикла и его применение.

В языке Си можно выделить несколько основных управляющих конструкций.

Операция присваивания

Сначала рассмотрим одну из них - операцию присваивания (=). Выражение вида

х = у;

присваивает переменной х значение переменной у. Операцию "=" разрешается использовать многократно в одном выражении, например:

x = y = z = 100;

Условный оператор if ... else. Форма оператора следующая:

if ( условие )

оператор1

else

оператор2

Если условие истинно, то выполнятся первый оператор, иначе второй. Если в условии отрабатываются несколько операторов, то они помещаются фигурные скобки. Вторая часть (else) может опускаться если нам не нужно обрабатывать ложное условие. Допускается вложение условных операторов.

Далее рассмотрим структуры цикла.

Итерационный цикл - цикл управляемый счетчиком.

Структура следующая:

for ( инициализация; условие; операция )

{

операторы

}

Первый параметр инициализирует счетчик, второй - условие при истиности которого выполняются операторы, третий - операция выполняемая перед новой итерацией.

Цикл с предусловием - цикл управляемый условием.

Структура следующая:

while ( условие )

{

операторы

}

Цикл выполняется пока условие истинно (условие проверяется в начале).

Цикл с постусловием - цикл управляемый условием.

Структура следующая:

do {

операторы

} while ( условие )

Цикл выполняется пока условие истинно (условие проверяется в конце, т.е. тело цикла выпольняется по крайней мере один раз).

Оператор выбора switch. Форма оператора следующая:

switch (выражение) {

case константа_1 : операторы ; break;

...

case константа_n : операторы ; break;

default : операторы ; break;

}

Оператор switch вычисляет выражение и переходит к первому совпадающему значению после case. Далее выполняются операторы этого блока и по команде break происходит выход из структуры. Если ни одно из значений не совпадает с константами из case, то выполняются операторы блока default. Отметим, что константы в case блоке определяются на этапе компиляции, поэтому они не могут содержать переменных и функций.

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

Операторы break и continue. Использование оператора break мы уже видели на примере структуры switch. Оператор break - это выход из цикла или конструкции switch.

Оператор continue - переход на конец цикла (т.е. пропуск всех операторов от continue до конца структуры цикла).

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

Инварианты используются в теории верификации программ для доказательства правильности выполнения цикла. Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему:

1. Доказывается, что выражение инварианта истинно перед началом цикла.

2. Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении цикла инвариант будет выполняться.

3. Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).

4. Доказывается (возможно — без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.

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

Пример 1.

for (i=0; i<N; i++) A[i]=0;

Первые i элементов массива уже обнулены

Пример 2.

while (i<N) { if (A[i]!=0) s=s*A[i]; i++;}

Переменная s равна произведению первых i ненулевых элементов

Иными словами, инвариант — это выражение, которое остаётся неизменным перед выполнением цикла и в процессе его выполнения, причём выражение составляется из переменных цикла. Проверка правильности построения цикла на основе инварианта выглядит так: сначала доказываем истинность инварианта перед началом цикла, потом после выполнения цикла, потом проверяем правильность результирующих переменных инварианта, потом проверяем выполнимость условия окончания цикла, а на основе всего этого делаем вывод, что цикл составлен правильно.