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

Если вы читали «Should I check the parameters to my function? » в блоге Larry Osterman, и являетесь сторонником второго подхода – можете дальше не читать. :-)

Когда то давно, функции IsBadReadPtr и IsBadWritePtr использовались для проверки валидности переданных указателей. Правда, со временем выяснилось, что от этих функций больше вреда, чем пользы. Во-первых, вместо обнаружения некорректных указателей (что по идее было целью их создателей), эти функции скорее скрывали ошибки. Во-вторых, даже успешное тестирование указателя с помощью одной из функций не гарантировало успешность следующей операции с этой памятью в многозадачной среде. В-третьих, IsBadWritePtr портит память по фактически случайному адресу – гарантия того, что приложение всё-таки упадёт позднее, но только с большими неприятностями. В-четвёртых, даже IsBadReadPtr может быть виновником в сбое приложения, если проверяемый адрес приходится на зашитную страницу (guard page) стека. В результате система потеряет возможность увеличивать стек, по мере надобности, и приложение с грохотом упадёт, если попытается это сделать.

Как же правильно проверять переданные указатели? Правило простое – любое значение указателя не равное 0 считается корректным. Если указатель на самом деле указывает «не туда», то приложение завершиться ошибкой доступа, что, в общем-то, плохо, но помогает найти и исправить ошибки быстрее.

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

В случае ядерного вызова указатели должны проверяются на корректность, однако и в этом случае IsBadXxxPtr оказывается не у дел. NT ядро использует функции ProbeForRead и ProbeForWrite , которые во много похожи на IsBadXxxPtr. Не смотря на похожесть, ProbeForXxx главным образом проверяют, что переданный буфер целиком находится в пользовательском адресном пространстве, а не то, что буфер размещён в валидной памяти. Дальнейшие обращения к переданному буферу в любом случае окружаются блоком __try - __except. Иными словами такая проверка гарантирует, что пользовательский код не сможет заставить ядерный код обратится к какому-либо адресу в адресном пространстве ядра. Тем самым ситуация с порчей защитной страницы ядерного стека, как результат запроса из пользовательского кода, не возможна. Само собой, что защитная страница пользовательского стека по-прежнему может пострадать. Но тут уж само приложение виновато.

Этот раздел посвящен описанию промежуточного подхода. Основные практические решения изложены в лекции 17 .

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

каждая из них служит примером правильного применения важных ОО-механизмов: первая - полиморфизма, вторая - переопределения типов. Проблемы начинаются при объединении их для одной и той же сущностиs . Аналогично:

p.add_vertex (...)

проблемы начинаются с объединения двух независимых и совершенно невинных операторов.

Ошибочные вызовы ведут к нарушению типов. В первом примере полиморфное присваивание присоединяет объект BOY к сущностиs , что делаетg недопустимым аргументомshare , так как она связана с объектомGIRL . Во втором примере к сущностиr присоединяется объектRECTANGLE , что исключаетadd_vertex из числа экспортируемых компонентов.

Вот и идея нового решения: заранее - статически, при проверке типов компилятором или иными инструментальными средствами - определим набор типов (typeset) каждой сущности, включающий типы объектов, с которыми сущность может быть связана в период выполнения. Затем, опять же статически, мы убедимся в том, что каждый вызов является правильным для каждого элемента из наборов типов цели и аргументов.

В наших примерах оператор s:= b указывает на то, что классBOY принадлежит набору типов дляs (поскольку в результате выполнения инструкции созданияcreate b он принадлежит набору типов дляb ).GIRL , ввиду наличия инструкцииcreate g , принадлежит набору типов дляg . Но тогда вызовshare будет недопустим для целиs типаBOY и аргументаg типаGIRL . АналогичноRECTANGLE находится в наборе типов дляp , что обусловлено полиморфным присваиванием, однако, вызовadd_vertex дляp типаRECTANGLE окажется недопустимым.

Эти наблюдения наводят нас на мысль о создании глобального подхода на основе нового правила типизации:

Правило системной корректности

Вызов x.f (arg) является системно-корректным, если и только если он классово-корректен дляx , иarg , имеющих любые типы из своих соответствующих наборов типов.

В этом определении вызов считается классово-корректным, если он не нарушает правила Вызова Компонентов, которое гласит: еслиC есть базовый класс типаx , компонентf должен экспортироватьсяC , а типarg должен быть совместим с типом формального параметраf . (Вспомните: для простоты мы полагаем, что каждый подпрограмма имеет только один параметр, однако, не составляет труда расширить действие правила на произвольное число аргументов.)

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

основные правила создания набора типов для каждой сущности: 1 Для каждой сущности начальный набор типов пуст.

2 Встретив очередную инструкцию видаcreate {SOME_TYPE} a , добавимSOME_TYPE в набор типов дляa . (Для простоты будем полагать, что любая инструкцияcreate a будет заменена инструкциейcreate {ATYPE} a , гдеATYPE - тип сущностиa .)

3 Встретив очередное присваивание видаa:= b , добавим в набор типов дляa все элементы набора типов дляb .

4 Еслиa есть формальный параметр подпрограммы, то, встретив очередной вызов с фактическим параметромb , добавим в набор типов дляa все элементы набора типов дляb .

5 Будем повторять шаги (3) и (4) до тех пор, пока наборы типов не перестанут изменяться. Данная формулировка не учитывает механизма универсальности, однако расширить

правило нужным образом можно без особых проблем. Шаг (5) необходим ввиду возможности цепочек присваивания и передач (от b кa , отc кb и т. д.). Нетрудно понять, что через конечное число шагов этот процесс прекратится.

|Число шагов ограничено длиной максимальной цепочки присоединений; другими словами максимум равен n , если система содержит присоединения отx i+1 кx i д л яi=1, 2, ... n-1 . Повторение шагов (3) и (4) известно как метод "неподвижной точки". |

Как вы, возможно, заметили, правило не учитывает последовательности инструкций. В случае

create {TYPE1} t; s:= t; create {TYPE2} t

в набор типов для s войдет какTYPE1 , так иTYPE2 , хотяs , учитывая последовательность инструкций, способен принимать значения только первого типа. Учет расположения инструкций потребует от компилятора глубокого анализа потока команд, что приведет к чрезмерному повышению уровня сложности алгоритма. Вместо этого применяются более пессимистичные правила: последовательность операций:

будет объявлена системно-некорректной, несмотря на то, что последовательность их выполнения не приводит к нарушению типа.

Глобальный анализ системы был (более детально) представлен в 22-й главе монографии . При этом была решена как проблема ковариантности, так и проблема ограничений экспорта при наследовании. Однако в этом подходе есть досадный практический недочет, а именно: предполагается проверкасистемы в целом , а не каждого класса в отдельности. Убийственным оказывается правило (4), которое при вызове библиотечной подпрограммы будет учитывать все ее возможные вызовы в других классах.

Хотя затем были предложены алгоритмы работы с отдельными классами в , их практическую ценность установить не удалось. Это означало, что в среде программирования, поддерживающей возрастающую компиляцию, необходимо будет организовать проверку всей системы. Желательно проверку вводить как элемент (быстрой) локальной обработки изменений, внесенных пользователем в некоторые классы. Хотя примеры применения глобального подхода

известны, - так, программисты на языке C используют инструмент lint для поиска несоответствий в системе, не обнаруживаемых компилятором, - все это выглядит не слишком привлекательно.

В итоге, как мне известно, проверка системной корректности осталась никем не реализованной. (Другой причиной такого исхода, возможно, послужила сложность самих правил проверки.)

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

Однако, несмотря на свое имя, фактически можно проверить системную корректность, используя только возрастающую проверку классов (в процессе работы обычного компилятора). Это и будет финальным вкладом в решение проблемы.

Все основные функции движка уже готовы. Во всяком случае, те, что отвечают за выборку контента и навигацию. Осталась одна деликатная тема: что делать, если кто-то запросил некорректный URL?

Статические сайты обслуживаются сервером - если запрошенный файл не найден, сервер выдаст заголовок (HTTP Response Header) с кодом статуса «404 Not Found». Но в случае динамического движка отдаваемый документ определяется не по имени файла в URL, а по переданным скрипту параметрам. При неверных параметрах файл скрипта все равно лежит на своем месте, значит сервер запустит его и отдаст код статуса «200 OK». А документа, соответствующего параметрам, нет. Поэтому скрипт должен определить некорректные парамеры и переписать код статуса до начала выдачи документа. И прекратить работу, не пытаясь искать несуществующие данные.

Для такого аварийного завершения нам потребуются всего две вещи. Первая - HTML-файл страницы с сообщением об ошибке - для выдачи в браузер пользователя. Приготовим его заранее и положим в корневую директорию сайта под именем 404.htm (так он у нас прописан в файле конфигурации).
Вторая - функция, которая отсылает HTTP-заголовок с кодом ошибки и прекращает работу скрипта. Выглядит она так:

Глобальные переменные $charset и $page404 определены в файле конфигурации. А параметр $pageout - логическая переменная, определяющая, выдавать страницу с сообщением об ошибке или нет. По умолчанию его значение FALSE - то есть функция только отдаст HTTP-заголовок с кодом статуса и прекратит работу. Версия протокола HTTP берется из переменной окружения SERVER_PROTOCOL, чтобы послать отклик именно с той версией, по которой работает сервер. Если функцию запустить с параметром TRUE, то после передачи заголовка она считает и отправит в поток вывода файл со страницей сообщения. Выдача только заголовка без сообщения может пригодиться в дальнейшем - в тех случаях, когда точно известно, что запрос послан не браузером, а роботом.

В директории /libs создаем файл functn.inc.php - в него помещаем функцию err404() и функцию hierarchy(), описанную в разделе Разбор структуры сайта . В тот же файл записываем функции выборки разделов для меню: getmain(), getsub() и getlevel(), описанные в разделе Выборка разделов для меню . Базовая библиотека готова. Теперь самое время провести проверку корректности запроса. Этот код уже пойдет в начало центрального скрипта main.php

В первых двух строках подгружается файл конфигурации и файл с функциями. Затем определяем логическую переменную $fakelink - она работает «флажком», который будет поднят при любом некорректном состоянии URL. Далее начинаем серию проверок.

Первое условие проводит проверку в случае, когда включен режим трансляции статических URL (переменная $urlmode не пустая и не равна "none"). Из переменной окружения REQUEST_URI берется первоначально запрошенный (не транслированный) URL и проверяется на отсутствие вопросительного знака. Если ссылки статические, его там быть не должно - статические URL параметров не имеют.

Второе условие:

  • при наличии GET-параметров (в случае статических ссылок они появляются после трансляции URL) перебирается в цикле массив $_GET. В ходе перебора наименование каждого параметра проверяется на наличие такого имени в массиве разрешенных (массив определен в файле конфигурации). Неизвестное имя параметра вызывает взвод флажка $fakelink в состояние TRUE и выход из цикла. Попутно создаются переменные с теми же именами и теми же значениями, что и у параметров. Возможные пробельные символы в значениях отсекаются.
  • при отсутствии GET-параметров считаем, что было обращение к корню сайта. Проверяется переменная окружения QUERY_STRING - она в этом случае должна быть пустой. Но туда могут попасть кое-какие нелепые довески к запросу корня, не попадающие в $_GET - наподобие http://domain.ru/?=

После первых двух проверок нужно остановить работу скрипта, если запрошенный URL некорректен. Что мы и делаем - при поднятом флажке $fakelink запускается передача статуса «404 Not Found» с завершением работы скрипта.

Далее, если URL корректного формата, считывается структура сайта и формируется массив разделов. И тут же следует третья проверка - если в массиве разделов не обнаружен алиас запрошенного раздела, значит пришел запрос с корректным форматом, но запрошенная страница не существует. В этом случае также выдается статус 404 и скрипт завершает работу.

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

Аннотация: Программные системы во многих случаях – жизненно важные системы, от правильной работы которых может зависеть благосостояние и даже жизнь отдельного человека или целого коллектива. Элементами доказательного программирования должен владеть каждый профессиональный программист. В этой же лекции обсуждаются вопросы и профессионального стиля разработки программных проектов. Лекция сопровождается задачами.

Проект к данной лекции Вы можете скачать .

Корректность и устойчивость

Корректность и устойчивость - два основных качества программной системы, без которых все остальные ее достоинства не имеют особого смысла.

Корректность - это способность программной системы работать в строгом соответствии со своей спецификацией. Отладка - процесс, направленный на достижение корректности.

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

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

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

Почему так трудно создавать корректные и устойчивые программные системы? Все дело в сложности разрабатываемых систем. Когда в 60-х годах прошлого века фирмой IBM создавалась операционная система OS-360 , то на ее создание потребовалось 5000 человеко-лет, и проект по сложности сравнивался с проектом высадки первого человека на Луну. Сложность нынешних сетевых операционных систем, систем управления хранилищами данных, прикладных систем программирования на порядок превосходит сложность OS-360 , так что, несмотря на прогресс, достигнутый в области технологии программирования, проблемы, стоящие перед разработчиками, не стали проще.

Жизненный цикл программной системы

Под " жизненным циклом " понимается период от замысла программного продукта до его "кончины". Обычно рассматриваются следующие фазы этого процесса:

Проектирование Разработка Развертывание и Сопровождение

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

Вот некоторые типовые правила, характерные для процесса разработки ПО .

  • Уделяйте этапу проектирования самое пристальное внимание. Успех дела во многом определяется первым этапом. Нет смысла торопиться с переходом на последующие этапы, пока не составлены ясные и четкие спецификации. Ошибки этого этапа- самые дорогие и трудно исправляемые.
  • Помните о тех, для кого разрабатывается программный продукт. Идите "в люди", чтобы понять, что нужно делать. Вместе с тем не следует полностью полагаться на пользователей - их опыт консервативен, новые идеи могут часто приходить от разработчиков, а не от пользователей.
  • Разработка не начинается "с нуля". Только используя уже готовые компоненты, можно своевременно создать новую систему. Работая над проектом, думайте о будущем создавайте компоненты, допускающие их повторное использование в других проектах.
  • Создавайте как можно раньше прототип своей системы и передавайте его пользователям в опытную эксплуатацию. Это поможет устранить множество недостатков и ошибок в заключительной версии программного продукта.
  • Какие бы хорошие спецификации не были написаны, какими бы хорошими технологиями и инструментами не пользовались разработчики, какими бы профессионалами они ни были - этого еще не достаточно для успеха дела. Необходимым условием является управление проектом, наличие специальных средств управления. Но и этого не достаточно. Третьим важным фактором является существование команды. Коллектив разработчиков должен представлять собой единый коллектив. Умение работать в команде так же важно, как и профессиональные навыки разработчика.
Три закона программотехники Первый закон (закон для разработчика)

Корректность системы - недостижима. Каждая последняя найденная ошибка является предпоследней .

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

Второй закон (закон для пользователя)

Не бывает некорректных систем. Каждая появляющаяся ошибка при эксплуатации системы - это следствие незнания спецификации системы .

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

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

Обратите внимание на философию, характерную для этих законов: при возникновении ошибки разработчик и пользователь должны винить себя, а не кивать друг на друга. Так что часто встречающиеся фразы: "Ох, уж эта фирма Чейтософт, вечно у них ошибки!" характеризует, мягко говоря, непрофессионализм пользователя.

Третий закон (закон чечако)

Если спецификацию можно нарушить, она будет нарушена. Новичок (чечако) способен "подвесить" любую систему .

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

Надежный код

Что должно делать для создания корректного и устойчивого программного продукта? Как минимум , необходимо:

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

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

Для повышения надежности нужно уменьшить сложность системы, и главное в этом процессе - это повторное использование . В идеале большая часть системы должна быть собрана из уже готовых компонентов. Объектная технология проектирования вносит свой вклад в повышение надежности кода. Наследование и универсализация позволяют, не изменяя уже существующие классы, создать новые классы, новые типы данных, придающие проектируемой системе новые свойства при минимальных добавлениях нового кода. Статический контроль типов дает возможность выявить многие ошибки еще на этапе компиляции. Динамическое связывание и полиморфизм позволяют автоматически включать объекты классов-потомков в уже существующие схемы работы - методы родителя могут вызывать методы потомков, не зная о появлении этих новых потомков. Автоматическая сборка мусора дает возможность снять с разработчика обязанности управления освобождением памяти и предотвратить появление крайне неприятных и опасных ошибок, связанных с некорректным удалением объектов.

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

Написать программную систему нетрудно. Это может сделать каждый. Значительно сложнее написать ее так, чтобы она корректно решала задачи пользователя. Корректность системы - это не внутреннее понятие, подлежащее определению в терминах самой системы. Корректность определяется по отношению к внешним спецификациям системы. Если нет спецификаций, то говорить о корректности "некорректно".

Корректность методов

Спецификации метода можно задавать по -разному. Определим их здесь через понятия предусловий и постусловий метода, используя символику триад Xoара, введенных Чарльзом Энтони Хоаром - выдающимся программистом и ученым.

Пусть P(x,z) - метод P с входными аргументами x и выходными z . Пусть Q(y) - некоторое логическое условие ( предикат ) над переменными y . Предусловием метода P(x,z) будем называть предикат Pre(x) , заданный на входах метода. Постусловием метода P(x,z) будем называть предикат Post(x,z) , связывающий входы и выходы метода. Для простоты будем полагать, что метод P не изменяет своих входов x в процессе своей работы. Теперь несколько определений:

Определение 1 (частичной корректности ). Метод P(x,z) корректен (частично, или условно) по отношению к предусловию Pre(x) и постусловию Post(x,z) , если из истинности предиката Pre(x) следует, что для метода P(x,z) , запущенного на входе x , гарантируется выполнение предиката Post(x,z) при условии завершения метода на этом входе.

Условие частичной корректности записывается в виде триады Хоара, связывающей метод с его предусловием и постусловием:

P(x,z)

Определение 2 (полной корректности ). Метод P(x,z) корректен (полностью, или тотально) по отношению к предусловию Pre(x) и постусловию Post(x,z) , если из истинности предиката Pre(x) следует, что для метода P(x,z) , запущенного на входе x , гарантируется его завершение и выполнение предиката Post(x,z) в точке завершения метода.

Условие полной корректности записывается в виде триады Хоара, связывающей программу с ее предусловием и постусловием:

{Pre(x)}P(x,z){Post(x,z)}

Доказательство полной корректности обычно состоит из двух независимых этапов - доказательства частичной корректности и доказательства завершаемости программы. Заметьте, полностью корректная программа , которая запущена на входе, не удовлетворяющем ее предусловию, вправе зацикливаться, вправе возвращать любой результат. Любая программа корректна по отношению к предусловию, заданному тождественно ложным предикатом False . Любая завершающаяся программа корректна по отношению к постусловию, заданному тождественно истинным предикатом True .

Корректная программа говорит своим клиентам: если вы хотите вызвать меня и ждете гарантии выполнения постусловия после моего завершения, то будьте добры гарантировать выполнение предусловия на входе. Задание предусловий и постусловий методов - это такая же важная часть работы программиста, как и написание самого метода. На языке C# пред- и постусловия обычно задаются в теге summary , предшествующем методу, и являются частью XML-отчета . К сожалению, технология работы в Visual Studio не предусматривает возможности автоматической проверки предусловия перед вызовом метода и проверки постусловия после его завершения с выбрасыванием исключений в случае их невыполнения. Программисты, для которых требование корректности является важнейшим условием качества их работы, сами встраивают такую проверку в свои программы. Как правило, подобная проверка обязательна на этапе отладки и может быть отключена в готовой системе, в корректности которой программист уже уверен. А вот проверку предусловий важно оставлять и в готовой системе, поскольку истинность предусловий должен гарантировать не разработчик метода, а клиент, вызывающий метод. Клиентам же свойственно ошибаться и вызывать метод в неподходящих условиях.

Формальное доказательство корректности метода - задача ничуть не проще, чем написание корректной программы. Но вот парадокс. Чем сложнее метод, его алгоритм , а следовательно, и само доказательство , тем важнее использовать понятия предусловий и постусловий, понятия инвариантов циклов в процессе разработки метода. Рассмотрение этих понятий параллельно с разработкой метода может существенно облегчить построение корректного метода.

Инварианты и варианты цикла

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

Рассмотрим цикл в форме, к которой можно привести все виды циклов:

Init(x,z); while(B)S(x,z);

Здесь B - условие цикла while , S - его тело, а Init - группа предшествующих операторов, задающая инициализацию цикла. Реально ни один цикл не обходится без инициализирующей части. Синтаксически было бы правильно, чтобы Init являлся бы формальной частью оператора цикла. В операторе for это частично сделано - инициализация счетчиков является частью цикла.

Определение 3 (инварианта цикла ). Предикат Inv(x, z) называется инвариантом цикла while , если истинна следующая триада Хоара:

{Inv(x, z)& B}S(x,z){Inv(x,z)}

Для любого цикла можно написать сколь угодно много инвариантов. Любое тождественное условие (2*2 =4) является инвариантом любого цикла. Поэтому среди инвариантов выделяются так называемые подходящие инварианты цикла. Они называются подходящими, поскольку позволяют доказать корректность цикла по отношению к его пред- и постусловиям. Как доказать корректность цикла? Рассмотрим соответствующую триаду:

{Pre(x)} Init(x,z); while(B)S(x,z);{Post(x,z)}

Доказательство разбивается на три этапа. Вначале доказываем истинность триады:

(*) {Pre(x)} Init(x,z){RealInv(x,z)}

(**) {RealInv(x, z)& B} S(x,z){ RealInv(x,z)}

На последнем шаге доказывается, что наш инвариант обеспечивает решение задачи после завершения цикла:

for(i = 1; i