Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и аппарат вывода. Правила доказательства являются громоздкими и поэтому на практике редко используются рядовыми программистами. Однако с теоретической точки зрения они развивают логику применения математического метода индукции при проверке правильности программ. На основеспецификации программ проводится частичное и полное доказательство правильности программ [6.4, 6.5].
Под доказательством частичной правильности понимается проверка выполнения свойств данных программы с помощью утверждений, которые описывают то, что должна получить эта программа, когда закончится ее выполнение в соответствии с условиями заключительного утверждения. Полностью правильной программой по отношению к ее описанию и заданным утверждениям будет программа, если она частично правильная и заканчивается ее выполнение при всех данных, удовлетворяющих ей.
Лекция 73: Реализация функции бинарного поиска на языке C с доказательством правильности программы
Для доказательства частичной правильности используется метод индуктивных утверждений, сущность которого состоит в следующем. Пусть утверждение связано с началом программы, — с конечной точкой программы и утверждение отражает некоторые закономерности значений переменных, по крайней мере, в одной из точек каждого замкнутого пути в программе (например, в циклах). Если при выполнении программа попадает в -ю точку и справедливо утверждение , а затем она проходит от точки к точке , то будет справедливо утверждение .
Теорема 6.1. Если выполнены все действия метода индуктивных утверждений для программы, то она частично правильна относительно утверждений , , .
Требуется доказать что, если выполнение программы закончится, то утверждение будет справедливым. По индукции, при прохождении точек программы, в которых утверждение будет справедливым, то и -я точка программы будет такой же. Таким образом, если программа прошла -точку и утверждения и справедливы, то тогда, попадая из -ой точки в точку, утверждение будет справедливым, что и требовалось доказать.
Нравится 0
Понравилась работу? Лайкни ее и оставь свой комментарий!
Для автора это очень важно, это стимулирует его на новое творчество!
Посоветуйте статью друзьям!
Случайные работы
Другие работы автора
Проектирование ПО (Software design)
Надежность систем
Сопровождение ПО (Software maintenance)
Надежность систем
Управление инженерией ПО
Надежность систем
Характеристика областей знаний SWEBOK
Надежность систем
Подходы к верификации моделей
Надежность систем
Перспективные направления верификации программ
Надежность систем
Конструирование ПО (Software Construction)
Надежность систем
Тестирование ПО (Software Testing)
Надежность систем
Логистика на автомобильном транспорте
Надежность систем
Процесс инженерии ПО (Software Engineering Process)
Надежность систем
Методы и инструменты инженерии ПО
Лекция 23: Доказательство свойств программ
Надежность систем
Спецификации задач концепторным языком
Надежность систем
Жизненный цикл ПС, связь с ядром знаний SWEBOK
Надежность систем
Процессы ЖЦ верификация и валидация программ
Надежность систем
Похожие работы
Раздел 3 ФУНКЦИОНАЛЬНЫЕ СТИЛИ СОВРЕМЕННОГО РУССКОГО ЯЗЫКА
Риторика
Статус государственного служащего: права, обязанности, ограничения и запреты.
Политология
Международные правовые акты, международные договоры РФ как источники государственного права.
Политология
Билеты на ГКК для матросов 2 класса.
Иностранные языки
Команды, поданные наруль, рулевой обязан повторить, а вахтенный офицер должен убедиться, что они выполняются немедленно и аккуратно.
Иностранные языки
Источник: lektsia.info
Доказательство правильности программ
ДОКАЗАТЕЛЬСТВО ПРАВИЛЬНОСТИ ПРОГРАММ Программные ошибки как правило
Программные ошибки, как правило, делятся на три вида: Синтаксическая ошибка. Неправильное употребление синтаксических конструкций. Например, употребление оператора цикла for без () и <>. Семантическая ошибка. Нарушение семантики той или иной конструкции, например передача функции параметров, не соответствующих ее аргументам.
Логическая ошибка. Нарушение логики программы, приводящее к неверному результату.
Методы доказательства правильности программ 1) Отладка — это специальный этап в разработке программы, состоящий в выявлении и устранении программных ошибок, факт существования которых уже установлен. 2) Тестирование – процесс выполнения программы с намерением найти ошибку, а не подтвердить правильность программы.
Проверяемую программу неоднократно запускают с теми входными данными, относительно которых результат известен заранее. Затем сравнивают полученный машиной результат с ожидаемым. Если во всех случаях тестирования результат одинаковы, то вероятнее всего исходная программа работает правильно. 3) Метод установления правильности программ при помощи строгих средств известен как верификация программ. В отличие от тестирования программ, где анализируются свойства отдельных процессов выполнения программы, верификация имеет дело со свойствами программ.
Верификация (подтверждение правильности) – состоит в проверке и доказательстве корректности разработанной программы по отношению к совокупности формальных утверждений, представленных в спецификации и полностью определяющей связь между входными и выходными данными этой программы. При этом отношения между переменными н входе и выходе программы анализируется не в виде значений, как при тестировании, а в виде описаний их свойств, проявляющихся при любых процессах обработок этих переменных контролируемой в программе.
Верификация программы в принципе исключает необходимость её тестирования и отладки, так как при этом на более высоком уровне понятий и описаний всех переменных, устанавливается корректность процессов, их обработка и преобразования. Сущность каждой программы можно представить описаниями отношений между входными и выходными данными.
Эти отношения формализуются 1 программной спецификации. В реальных разработках формализация этих взаимосвязей является неплохой, и часть отношений уточняется в процессе разработок программ. Такие не полностью определённые недостаточны для доказательства корректности программ. Только при полной и точной формализации всех условий и связей между входными и результирующими данными появляется возможность их использования для автоматической верификации.
Доказательство правильности это подтверждение того, что семантика программы соответствует предъявляемым требованиям, изложенным в спецификации этой программы.
Зачем нужна проверка правильности программ? Возрастание стоимости ущерба из-за пропущенной ошибки в программе. 4 июня 1996 года европейская космическая ракета «Ариан 5» взорвалась менее чем через сорок секунд после запуска. Комиссия, расследовавшая аварию, обнаружила, что ее причиной послужила ошибка в программе компьютера, отвечавшего за расчеты движения ракеты.
В ходе запуска возникла ситуация, когда большое 64 -разрядное число с плавающей точкой было преобразовано в 16 -разрядное целое число. Это преобразование не было защищено кодом для обработки исключительных ситуаций, что и привело к сбою компьютера. Та же самая ошибка привела к сбою дублирующего компьютера. В результате на бортовой компьютер ракеты были переданы неверные данные о высоте, что вызвало уничтожение ракеты. 1.
Аппаратные и программные системы широко используются во многих приложениях, где любой отказ считается недопустимым: — энергетика; — электронная коммерция; — телекоммуникация; — системы управления воздушным и дорожным движением; — нефтегазовая промышленность; — медицинская аппаратура; — и прочие.
Зачем нужна проверка правильности программ? 2. Расширение области применения программ. Ежедневно возрастает участие программных систем в нашей жизни. В тоже время возрастает ответственность за правильность их функционирования. Мы становимся зависимыми от правильности функционирования вычислительных устройств.
Изменяется само понимание задачи проверки правильности программ: программа может быть признана надежной не потому, что в ней не удалось обнаружить ошибок, а потому, что удалось убедительно доказать отсутствие ошибок.
Зачем нужна проверка правильности программ? 3. Возрастание трудоемкости проверки правильности программ. Вычислительная аппаратура становится дешевле, а производительность компьютеров возрастает. Появляются новые возможности автоматического решения все более и более сложных задач. Происходит увеличение объемов программного кода.
Основные подходы к задаче верификации Основными методами проверки правильности сложных систем (программ и микроэлектронной аппаратуры) являются имитационное моделирование и тестирование. Имитационному моделированию подвергается абстрактная схема или прототип, тестирование применяется непосредственно к самому продукту. В обоих случаях в этих методах определенные сигналы обычно вводятся в заданных точках схемы, а в других точках снимают соответствующие показания. Эти методы могут быть весьма экономичны для выявления многих ошибок. Однако проверить ВСЕ возможные взаимодействия и обойти ВСЕ «ловушки» , применяя лишь моделирование и тестирование, не удастся.
Формальные методы верификации предназначены не для доказательства того, что в проектируемой системе НЕТ ошибок определенного вида. Основные подходы к формальной проверке правильности сложных управляющих систем: 1) Проверка эквивалентности. 2) Дедуктивный анализ. 3) Верификация моделей программ.
1) Проверка эквивалентности.
2) Дедуктивный анализ.
Дедуктивный метод оказал значительное влияние на подходы к разработке программного обеспечения (например, понятие инварианта заимствовано из исследований по дедуктивному анализу). Тем не менее, он требует чересчур много времени и может быть осуществлен только экспертами, обладающим знаниями в области логического вывода и имеющими немалый практический опыт. Доказательство правильности отдельного протокола или электронной схемы может занять целые дни или даже месяцы. Поэтому дедуктивный анализ используется главным образом для проверки систем, наиболее чувствительных к сбоям, наподобие протоколов защиты, когда можно выделить необходимые ресурсы, для того чтобы гарантировать их безопасное использование.
3) Верификация моделей программ.
Принципы model checking:
Темпоральная логика и модели
Источник: present5.com