Cтраница 2
ПРОГРАММ ВЕРИФИКАЦИЯ - направление программирования теоретического, связанное с разработкой и изучением методов доказательства правильности программ, ориентированных на практическое применение, в частности на программ синтез. [16]
Здесь рассмотрены некоторые правила тестирования, в которых делается попытка учесть как желательность доказательства правильности контролируемой программы, так и ограниченность человеческих возможностей при проведении такого доказательства. [17]
Однако в указанной главе эта проблема обсуждается на более высоком уровне - с позиций теории доказательства правильности программ, базирующейся на иерархии математических функций. [18]
Использование побочного эффекта нежелательно, поскольку он сильно затрудняет ( особенно, если не предусмотрен заранее) отладку и доказательство правильности программы. [19]
Причиной увеличения Z ( t) является то, что процесс обнаружения и исправления ошибок рассматривается как цепь последовательных попыток доказательства правильности программы. Чем выше интенсивность тестирования, тем больше уверенность в том, что очередные ошибки вызываются лишь редкими комбинациями входных данных, позволяющих проверить все новые и новые пути программы. [20]
В первом разделе отмечалось, что формулировка индуктивных утверждений внутри каждого цикла - это, вероятно, самое тяжелое бремя в доказательстве правильности программы. Несколько исследовательских работ было посвящено попытке автоматизировать генерацию индуктивных утверждений. [21]
Оглядываясь назад, можно отметить, что решение нарушить широко распространенную традицию выглядит опрометчивым, особенно вследствие роста значения сложных булевских выражений в связи с доказательством правильности программ. [22]
Выявить те особенности языков программирования, которые находят наиболее широкое использование, и оценить их в терминах их спецификаций, вызываемых ими эффектов, их практического использования, возмож ности доказательства правильности программ, соответствия потребностям программиста. [23]
В этих подходах имеется ряд ограничений. Доказательство правильности программ возможно лишь для небольших и простых программ. Отладка и тестирование программ может лишь показать наличие ошибок, а не их отсутствие. Структурное программирование достигло в некоторой степени успехов при построении нескольких систем, оказавшихся вполне надежными при их внедрении. Однако для их надежной оценки еще не накоплено достаточно опыта. [24]
Следует обратить внимание на то, что доказательство общей правильности программы проводится не путем анализа результатов ее прогона, а на основе анализа программы, как статического математического объекта, на который распространяются аксиомы и правила логического вывода. Основной проблемой доказательства правильности программы является формирование вспомогательных утверждений. Для этого требуется тщательный учет структуры программы и семантики языка программирования. Построения вспомогательных утверждений для некоторой произвольной программы зачастую оказываются очень сложной и конструктивной задачей, поэтому определенные преимущества достигаются тогда, когда процедуры доказательства и правильности программы разрабатываются в процессе ее проектирования. Чтобы доказать факт завершения работы программы, необходимо доказать, во-первых, что программа не остановлена преждевременно, и, во-вторых, что программа не зациклилась. Подтверждение первого факта может оказаться очень сложным, например, может возникнуть потребность в доказательстве того, что не будет происходить арифметического переполнения. Подтверждение того, что программа в конце концов выйдет из некоторого цикла, может быть основано на концепции вполне упорядоченного множества ( W. Допустим, например, что применительно к некоторому циклу выражение Е может быть найдено так, что если оно отрицательно, цикл немедленно завершится. Далее допустим, что может быть доказан факт уменьшения Е с каждой итерацией цикла. Из этого следует, что цикл должен завершиться. Доказательство правильности программы не дает полного решения проблемы надежности программного обеспечения практически используемых систем. [25]
Правильность программы определяется как соответствие между программой и ее заданной функцией. Для сведения задачи доказательства правильности определенной составной программы к задаче доказательства правильности определенных элементарных составляющих программ привлекают алгебраические понятия. Верификация правильности программ без циклов осуществляется с помощью анализа соответствующих Е - схем. Лемма о переходе от итеративных программ к рекурсивным позволяет свести задачу верификации циклических программ к задаче верификации эквивалентных программ без циклов. В теореме правильности обобщены требования к верификации, соответствующие ациклическим и циклическим элементарным программам. Для доказательства правильности программ используются трассировочные таблицы и разделяющиеся условные правила. Теоретико-функциональный подход к верификации иллюстрируется несколькими примерами. Еще один способ доказательства правильности циклических программ основан на использовании инвариантов цикла. Инварианты применяются также в качестве вспомогательного средства документирования программ. Для определения инвариантов дана общая процедура, основанная на теореме об инварианте. Наконец, с целью углубления в процесс проектирования программ приводится метод вывода правильных программ, использующий функциональные уравнения элементарных программ, для которых существуют формальные решения. [26]
Такой подход к доказательству правильности программ называют интуитивным. При использовании такого подхода не принимаются во внимание алгебраические свойства структурированных программ. Однако здесь нашей целью является иллюстрация возможности доказательства правильности программ на естественном языке. [27]
В лагере прагматиков отмечают существенную потерю эффективности программ, свойственную глобальному подходу к обеспечению их надежности. В отсутствие формальных методов доказательства правильности практически ценных программ, считают сторонники прагматического подхода, следует ориентироваться на простые и легко контролируемые при отладке протоколы обмена данными между модулями программы, а сами модули должны иметь минимальные размеры. Отсюда - сопряженное с требованием надежности требование мобильности программ. [28]
Итак, мы имеем систематически записанные доказательства правильности программ типа последовательность и whiledo, в которых использованы массивы. Эти доказательства схожи с доказательствами правильности программ, оперирующих скалярными данными, однако они требуют большей изобретательности при выводе программной функции. [29]
Аналитический подход в первую очередь затрагивает тестирование и обоснование программ после того, как они написаны, чтобы повысить их надежность. Он включает традиционные методы отладки программ, средства доказательства правильности программ, различные средства автоматического тестирования. Конструктивный подход использует набор надежных программных средств для разработки надежного ПО, которые принято называть структурным программированием. Этот подход включает построение средств, использующих просмотр сверху вниз и формальные спецификации, и средства кодирования с применением простых управляющих структур. [30]