Правильность - программа
Cтраница 1
Правильность программы проверяется путем сравнения выведенной из машины информации с соответствующими результатами ручного контрольного просчета. [1]
Правильность программы определяется как соответствие между программой и ее заданной функцией. Для сведения задачи доказательства правильности определенной составной программы к задаче доказательства правильности определенных элементарных составляющих программ привлекают алгебраические понятия. Верификация правильности программ без циклов осуществляется с помощью анализа соответствующих Е - схем. Лемма о переходе от итеративных программ к рекурсивным позволяет свести задачу верификации циклических программ к задаче верификации эквивалентных программ без циклов. В теореме правильности обобщены требования к верификации, соответствующие ациклическим и циклическим элементарным программам. Для доказательства правильности программ используются трассировочные таблицы и разделяющиеся условные правила. Теоретико-функциональный подход к верификации иллюстрируется несколькими примерами. Еще один способ доказательства правильности циклических программ основан на использовании инвариантов цикла. Инварианты применяются также в качестве вспомогательного средства документирования программ. Для определения инвариантов дана общая процедура, основанная на теореме об инварианте. Наконец, с целью углубления в процесс проектирования программ приводится метод вывода правильных программ, использующий функциональные уравнения элементарных программ, для которых существуют формальные решения. [2]
Правильность программы в целом зависит от 1) корректности сведения программы к подзадачам и 2) правильности реализации подзадач. Этими вопросами можно заниматься независимо: при сведении задачи к подзадачам можно не думать об их реализации, при проверке реализаций можно не думать, как они используются. [3]
Правильность программы проверяется путем сравнения выведенной из машины информации с соответствующими результатами ручного контрольного просчета. [4]
Правильность программы доказывается только по отношению к входному и выходному утверждениям. Если выходное утверждение неправильно или неполно, может быть доказана правильность программы, а ошибки в ней останутся необнаруженными. Кроме того, ошибки, сделанные на более ранних этапах проектирования ( цели, внешний проект), не будут обнаружены при доказательстве. [5]
Правильность программы не определена вне области изменения данных, заданной спецификацией, и не зависит от динамики функционирования программ в реальном времени. [6]
Проверка правильности программы осуществляется составителем перед записью программы. [7]
Доказательство правильности программ, учитывающее основные, но не все возможные факторы. [8]
Проверка правильности программы еще не обеспечивает этойг правильности. Она лишь позволяет убедиться в правильности программы относительно выбранного теста ( в полной правильности, если тест полный, или в относительной - в противном случае) или обнаружить факт наличия ошибки. Далее следует работа по выявлению содержания ошибки и ее устранению. Эта работа носит название отладки программы. [9]
Доказательство правильности программ, имеющих дело с непоименованными данными, проводится аналогично доказательствам, приведенным выше, за исключением того, что операции над непоименованными данными представляются специальными операциями над списками. [10]
Следовательно, правильность программы, как полная, так и достаточная, не доказана. Причиной этого является тот факт, что область определения функции sub включает значения yQ, которые не обрабатываются должным образом программой SUB. Следовательно, необходимо переопределить либо программу SUB, либо функцию sub, либо то и другое. [11]
Математическое доказательство правильности программы, состоящее в выявлении соответствия логического поведения программы ее спецификациям. При этом логическое поведение определяется множеством формальных утверждений. [12]
 |
Второй шаг совершенствования программы. [13] |
При проверке правильности программы замечаем, что для значения степени загрязнения более 100 млн 1 ( для некоторого момента измерений) значение over увеличивается на единицу. Вполне очевидно, что необходимо зафиксировать начальное нулевое значение этой переменной. Поэтому необходимо производить начальную установку кмк-менной over вне цикла почасовой обработки измерений, чтобы количество отсчетов для первого часа было верным. [14]
В доказательстве правильности программ и аксиоматической семантике языков программирования - логическое выражение, которое должно быть истинно после выполнения некоторого действия, если перед выполнением этого действия было истинно соответствующее предусловие. [15]
Страницы: 1 2 3 4