5. Примеры спецификаций (например, для метода сортировки массива в возрастающем порядке

6. Понятие Инварианта. Инвариант цикла.

Инвариа́нтом в программировании называется логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.

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

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

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

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

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

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

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

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

6. Что такое защитное программирование? Перечислите пути реализации защитного программирования.

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

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

Этот подход отличается от традиционного, при котором сначала устанавливается факт явной ошибки, а потом делается попытка проследить за процессом её возникновения в обратном порядке.

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