Cтраница 1
Теорема правильности только определяет, что указанные отношения должны верифицироваться для того, чтобы доказать корректность программы. Однако она используется в различных математических процедурах, а способ ее доказательства позволяет демонстрировать искомые зависимости. [1]
Теорема правильности показывает, что все структурированные программы, выраженные через элементарные, содержащие не более одного предиката, могут быть верифицированы ( за исключением вопроса окончания программ) посредством применения методов рассуждения, требуемых для программ типа последовательность и ifthen-else. Проблемы доказательства правильности могут оказаться слишком трудоемкими, но теоретически они разрешимы. [2]
В частности, теорема правильности требует определения заданной функции ( f), программы, доказательства и результата доказательства, идентифицируемых ключевыми словами function, program, proof и result соответственно. [3]
Тогда, применяя теорему правильности, можно проверить, что уравнение whiledo удовлетворяется. [4]
Для лучшей документации и связи аргументов доказательства изложенные в теореме правильности требования к доказательству корректности элементарных программ включают пункт к стандартной форме самих доказательств. Далее мы приводим как расширение внешнего синтаксиса языка PDL ключевые слова и правила записи частей доказательств для элементарных программ. Элементы внутреннего синтаксиса определяются и записываются на любом уровне, подходящем для рассматриваемых программы и доказательства. [5]
Инварианты, если они известны, можно использовать как альтернативу методам верификации, описанным в теореме правильности. Инвариантное отношение, помещаемое между ключевым словом while и while - тестом, является условием, которое должно удовлетворяться независимо от того, какое значение - истинно или ложно - принимает while - тест. [6]
Раздел proof доказательства предназначается и специализуется для каждой элементарной программы согласно виду условия С ( X, Y) в теореме правильности. Чтобы более компактно сформулировать правила доказательства, мы записываем условие С в виде сравнений условных правил. [7]
Верификация правильности ациклических программ выполняется путем их анализа и замещения. Формулируется лемма о преобразовании итеративных программ в рекурсивные, которая позволяет свести верификацию циклических программ к верификации ациклических программ. Теорема правильности программ обобщает требования верификации для структур языка PDL: приведены формальный и неформальный методы доказательства этой теоремы. Теорема об инварианте дает систематическое средство вывода инвариантов цикла. Описывается метод доказательства правильности программ, основанный на инвариантах. Рассматриваются теоретические методы получения эффективных программ. [8]
Правильность программы определяется как соответствие между программой и ее заданной функцией. Для сведения задачи доказательства правильности определенной составной программы к задаче доказательства правильности определенных элементарных составляющих программ привлекают алгебраические понятия. Верификация правильности программ без циклов осуществляется с помощью анализа соответствующих Е - схем. Лемма о переходе от итеративных программ к рекурсивным позволяет свести задачу верификации циклических программ к задаче верификации эквивалентных программ без циклов. В теореме правильности обобщены требования к верификации, соответствующие ациклическим и циклическим элементарным программам. Для доказательства правильности программ используются трассировочные таблицы и разделяющиеся условные правила. Теоретико-функциональный подход к верификации иллюстрируется несколькими примерами. Еще один способ доказательства правильности циклических программ основан на использовании инвариантов цикла. Инварианты применяются также в качестве вспомогательного средства документирования программ. Для определения инвариантов дана общая процедура, основанная на теореме об инварианте. Наконец, с целью углубления в процесс проектирования программ приводится метод вывода правильных программ, использующий функциональные уравнения элементарных программ, для которых существуют формальные решения. [9]
Рассмотрим доказательство правильности элементарных программ на примерах программ, оперирующих скалярными данными. Структуры типа fordo и case обсуждению не подлежат. Доказательство для структуры fordo было рассмотрено выше, а доказательство для структуры типа case является простым обобщением доказательства правильности программы типа ifthenelse. Доказательство правильности программ, использующих данные в виде массива и непоименованные данные, рассматриваются в следующем разделе. Доказательства удовлетворяют верификационным требованиям, определенным теоремой правильности, и записываются в соответствии с синтаксисом доказательства ( см. разд. Чтобы полнее проиллюстрировать оба систематических метода записи данных в трассировочные таблицы и применение логических правил рассуждения, доказательства записываются со всеми синтаксическими и логическими подробностями. Полная правильность доказывается для каждой программы, за исключением программы типа dowhiledo, при доказательстве которой обнаруживается ошибка в программе. [10]
Исключая случаи небулева предиката и применения выражения, которое не является функцией, ошибка типа обнаружилась бы в денотационной семантике только при применении примитивной функции к объекту неподходящего типа; при этом допустимые типы аргументов задаются спецификациями примитивных функций. W, например) не может привести к такой ошибке типа, и поэтому приведенные выше уравнения являются действительно достаточными. Фактически программа проверки типов, конечно, нашла бы любую ошибку типа, возникающую при применении выражения, ие являющегося функцией, и если бы мы представляли условные выражения с помощью примитивной функции от трех аргументов cond: truvai - - а - - а - - а, то могли бы вообще не говорить о типах в семантических уравнениях; программа проверки типов нашла бы также любые ошибки типов в условных выражениях. Однако это не означает, что семантика типов не является важной. Наоборот, приведенные выше аргументы зависят от теоремы семантической правильности для правильно типизированных выражений, при доказательстве которой типы представляются как поддомены семантического домена D с определенными свойствами. [11]