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

Раздел раскрывает смысл доказательного подхода и его связь с алгоритмами, логикой и спецификациями. Объясняется различие между утверждением «программа сработала на примере» и обоснованием того, что она удовлетворяет требованиям на всём заданном множестве входных данных. Уточняются условия, от которых зависит любое доказательство.

В пункте рассматриваются предусловия и постусловия как точное описание требований к команде или алгоритму. На простых примерах поясняется запись {P} C {Q}, где P задаёт исходные условия, C обозначает программу, а Q — ожидаемый результат. Также обсуждается, почему неполная или неоднозначная спецификация мешает проверке корректности.

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

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

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

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

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

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

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