Студопедия
Случайная страница | ТОМ-1 | ТОМ-2 | ТОМ-3
АрхитектураБиологияГеографияДругоеИностранные языки
ИнформатикаИсторияКультураЛитератураМатематика
МедицинаМеханикаОбразованиеОхрана трудаПедагогика
ПолитикаПравоПрограммированиеПсихологияРелигия
СоциологияСпортСтроительствоФизикаФилософия
ФинансыХимияЭкологияЭкономикаЭлектроника

Обоснования программ. Формализация свойств программ.

Завершимость выполнения программы. | Пример доказательства свойства программы | Принципы и виды отладки. | Заповеди отладки. | Автономная отладка модуля. | Комплексная отладка программного средства. | Обеспечение завершенности программного средства. | Обеспечение устойчивости программного средства. | Обеспечение защищенности программных средств. | Общая характеристика процесса обеспечения качества программного средства. |


Читайте также:
  1. Sp-Гибридизованное состояние свойственно атому, если сумма числа связанных с ним атомов и числа его неподеленных электронных пар равна 2
  2. Z-преобразование и его свойства
  3. А. Генетический код и его свойства
  4. А. ХАРАКТЕРНЫЕ СВОЙСТВА КАЖДОГО ОРГАНА
  5. агнитные свойства веществ. Магнитная проницаемость. Ферромагнетики.
  6. Адаптация - ориентация на подвижность, отсутствие инертности и быстрое приспособление к изменениям внешней социальной среды, свойств личности и коллектива.
  7. Адаптация 2.Бурдье 3.общество 4.система 5.познание 6.структура 7.экономика 8. Парсонс 9.свойства 10 политика 11.закон 12.сознание 13.схема 14.функция 15.право 16.коллектив

Для повышения надежности программных средств весьма полезно снабжать программы дополнительной информацией, с использованием которой можно существенно повысить уровень контроля ПС. Такую информацию можно задавать в форме неформализованных или формализо­ванных утверждений, привязываемых к различным фрагментам программ. Будем называть такие утверждения обоснованиями программы. Неформализованные обоснования программ могут, например, объяснять мотивы принятия тех или иных решений, что может существенно облегчить поиск и исправление ошибок, а также изучение программ при их сопровождении. Формализован­ные же обоснования позволяют доказывать некоторые свойства программ как вручную, так и контролировать (устанавливать) их автоматически.

Одной из используемых в настоящее время концепций формальных обоснований программ является использование так называемых триад Хоора. Пусть S - некоторый обобщенный оператор над информационной средой IS, P и Q - некоторые предикаты (утверждения) над этой средой. Тогда запись {P}S{Q} и называют триадой Хоора, в которой предикат P называют предусловием, а предикат Q - постусловием относительно оператора S. Говорят, что оператор (в частности, программа) S обладает свойством {P}S{Q}, если всякий раз, когда перед выполнением оператора S истинен предикат P, после выполнения этого оператора S будет истинен предикат Q. Простые примеры свойств программ:

(9.1) {n=0} n:=n+1 {n=1},

(9.2) {n<m} n:=n+k {n<m+k},

(9.3) {n<m+k} n:=3*n {n<3*(m+k)},

(9.4) {n>0} p:=1; m:=1;
ПОКА m /= n ДЕЛАТЬ
m:=m+1; p:=p*m

ВСЕ ПОКА

{p=n!}.

Для доказательства свойства программы S используются свойства простых операторов языка

программирования (мы здесь ограничимся пустым оператором и оператором присваивания) и

свойствами управляющих конструкций (композиций), с помощью которых строится программа из

простых операторов (мы здесь ограничимся тремя основными композициями структурного

программирования, см. Лекцию 8). Эти свойства называют обычно правилами верификации

программ.


Дата добавления: 2015-08-02; просмотров: 76 | Нарушение авторских прав


<== предыдущая страница | следующая страница ==>
Приложения| Свойства основных конструкций структурного программирования.

mybiblioteka.su - 2015-2024 год. (0.006 сек.)