Модель корректности программы - раздел Программирование, Предикатное программирование Рассмотрим Программу С Предикатной Спецификацией На Языке, Для Которого Можно...
Рассмотрим программу с предикатной спецификацией на языке, для которого можно построить логическую семантику. Программа со спецификацией представляется в виде тройки Хоара:
{P(x)} S {Q(x, y)} . (2.5)
Здесь программа представлена оператором S, x - набор входных данных, y - набор результатов.
Закон соответствия программы и спецификации, сформулированный в разд. 2.1, очевидным образом конкретизируется для программы с предикатной спецификацией в виде следующих условий:
· входные данные x должны соответствовать предусловию P(x) перед исполнением программы;
· входные данные x и результаты y должны удовлетворять постусловию Q(x, y) после завершения исполнения программы.
Во втором условии неявно подразумевается, что исполнение программы на входных данных x завершается. Более точная формулировка условия: если для набора x существует исполнение, завершающееся набором y, то истинно постусловие Q(x, y). Используя обозначения, введенные в разд. 2.2, запишем условие в виде формулы: RUN(S, x, y) Þ Q(x, y). Учитывая свойство согласованности (2.4), второе условие можно представить формулой: LS(S)(x, y) Þ Q(x, y). В итоге, закон соответствия программы и спецификации для программы с предикатной спецификацией выражается следующей формулой:
P(x) & ( LS(S)(x, y) Þ Q(x, y) ) . (2.6)
Замечание. Импликация в обратную сторону, т. е. Q(x, y) Þ LS(S)(x, y), в общем случае неверна. Во многих задачах спецификация Q(x, y) представляется более слабым (общим) условием, допускающим для фиксированного набора x не единственное решение y.
Предусловие P(x) не зависит от оператора S, поскольку значение P(x) определено до исполнения оператора S. Для программы в целом предусловие P(x) считается истинным априори. Истинность предусловия для случая, когда оператор S является частью программы, должна быть доказана, см. разд. 2.4 и 2.5. В любом случае, исполнение оператора S не рассматривается для ложного предусловия. Таким образом, истинность предусловия P(x) определяется как необходимое условие для тройки Хоара (2.5).
Закон соответствия программы и спецификации (2.6) определяет условие корректности программы (2.5). Однако первый конъюнкт P(x) не может входить в условие корректности оператора S, а второй конъюнкт реализуется при условии истинности P(x). Учитывая это, условие корректности программы представляется следующей формулой:
P(x) & LS(S)(x, y) Þ Q(x, y) . (2.7)
Предикат H(x, y) реализуем для конкретного x, если H(x, y) истинен для некоторого y, т. е. $y. H(x, y). Предикат H(x, y) реализуем в области предусловия P(x), если он реализуем для всех x, на которых истинно предусловие, т. е. "x. (P(x) Þ $y. H(x, y)). Предикат H(x, y) является тотальным в области предусловия, если рассматривать его как функцию, отображающую x в y. Спецификация в виде предусловия P(x) и постусловия Q(x, y) реализуема, если постусловие реализуемо в области предусловия.
Рассмотрим ситуацию, когда условие корректности (2.7) истинно, а спецификация нереализуема. Тогда для некоторого x истинно предусловие P(x), а постусловие Q(x, y) ложно для всех y. Из истинности (2.7) следует, что LS(S)(x, y) будет ложной для всех y. Как следствие свойства согласованности (2.4) получим, что "y ØRUN(S, x, y) истинно, т. е. исполнение оператора S для данного x не определено. Это означает, что исполнение либо реализуется бесконечно, либо завершается аварийно без получения результата. Подобная ситуация абсурдна в модели применения программы (см. рис. 1) – такое исполнение бессмысленно и не соответствует цели базового процесса.
Таким образом, мы приходим к следующему условию корректности спецификации: спецификация должна быть реализуема, т. е.:
P(x) Þ$y. Q(x, y) . (2.8)
Корректность спецификации является необходимым условием корректности программы, представленной тройкой (2.5).
Лемма 2.1. Спецификация с предусловием P(x) и постусловием Q(x, y) реализуема Û P(x) Þ PE(x).
Ситуация, когда для некоторого набора x, удовлетворяющего предусловию P(x), исполнение оператора S реализуется бесконечно или завершается аварийно без получения результата, т. е. "y. ØRUN(S, x, y), определена выше как недопустимая для программы с предикатной спецификацией. Следовательно, должно быть истинно обратное утверждение: $y. RUN(S, x, y), т. е. исполнение программы завершается с получением некоторого результата y. Данное утверждение эквивалентно $y. LS(S)(x, y), что следует из свойства согласованности (2.4). Таким образом, необходимым условием корректности программы является нормальное завершение исполнения программы для x, удовлетворяющего предусловию P(x). Условие корректности определяется формулой:
P(x) Þ $y. LS(S)(x, y) . (2.9)
Приведенные выше требования объединим в понятии корректности программы. Прежде всего, для программы (2.5) предусловие P(x) всегда истинно. Программа корректна, если спецификация реализуема (условие (2.8)), программа нормально завершается в области предусловия (условие (2.9)) и программа соответствует спецификации (условие (2.7)).
Лемма 2.2. Если программа соответствует спецификации и нормально завершается в области предусловия, то спецификация реализуема.
Доказательство. Пусть истинно P(x). Необходимо доказать истинность $y. Q(x, y). Из условия (2.9) следует истинность $y. LS(S)(x, y). Допустим, истинность этой формулы реализуется для некоторого y0. Из условия (2.7) получаем истинность Q(x, y0), а значит – и $y. Q(x, y). □
Таким образом, корректность программы (2.5) определяется двумя условиями: соответствие спецификации (2.7) и нормального завершения (2.9). Объединяя формулы (2.7) и (2.9), получаем итоговую формулу корректности программы:
Приведенное определение корректности программы соответствует общеизвестному понятию тотальной (или полной) корректности программы. Оно справедливо для программ с предикатной спецификацией и для языков программирования с логической семантикой. Основой данного определения корректности является формализация закона соответствия программы и спецификации для программ с предикатной спецификацией.
НОВОСИБИРСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ... Факультет информационных технологий...
Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ:
Модель корректности программы
Что будем делать с полученным материалом:
Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:
Новосибирск
УДК 004.432.42
ББК 22.183.492
Ш 427
Шелехов В. И. Предикатное программирование: Учеб. пособие / Новосиб. гос. ун-т. Новосибирск, 2009
Язык исчисления вычислимых предикатов,
его логическая и операционная семантика .......................................................... 27
4.1. Структура программы на языке CCP ...............................
Семантика языка предикатного программирования.
Методы доказательства корректности предикатных программ ...................... 47
5.1. Язык P1: подстановка определения предиката на место вызова .........................
Общее понятие программы
Понятие программы обычно определяется в контексте некоторого языка программирования. Представление об общем понятии программы, абстрагированное от конкретного языка программирования, для специалист
Автоматическая вычислимость
Развитие средств вычислений сопровождается все большей степенью автоматизации вычислений. Потребность в проведении сложных и длительных расчетов привела человека к необходимости создания и совершен
Спецификация программы
Для определения связи программы со своей спецификацией рассмотрим следующую модель применения программы (рис. 1). Вычисление по программе является необходимым звеном в цепочке действий некоторого р
Формы спецификации программы
Распространена точка зрения, что спецификацию программы можно представить в виде функции. Поскольку это не всегда так, возникает вопрос о классификации форм, которые может принимать спецификация пр
Корректность программ с предикатной спецификацией
Для класса программ с предикатной спецификацией рассматривается программа вместе со своей спецификацией. Введенное в предыдущем разделе понятие предикатной спецификации уточняется следующим образом
Предикатная спецификация программы
Уточним и дополним понятие предикатной спецификации, определенное в разд. 1.2. Рассмотрим следующую простую схему взаимодействия программы с окружением: ввод входных данных происходит перед началом
Логическая семантика языка программирования
Всякая программа содержит логику. Это, например, бизнес-логика, извлекаемая нетривиальным анализом из текста программы в процессе реинжиниринга программы [16]. Это также логические формулы, получае
Система правил вывода программы из спецификации
Понятие корректности программы, введенное в разд. 2.3, состоит из трех условий (2.7–2.9). Главным из них является условие (2.7) соответствия программы и спецификации, согласно которому постусл
Однозначность предикатов
Предикат H(x, y) является однозначным в области X для набора переменных x, если он определяет функцию, отображающую значения набора x в значения набора y. Должно быть истинным следующее усло
Теорема тождества спецификации и программы
Теорема определяет условия, при которых программа может быть выведена из спецификации.
Теорема 2.1 тождества спецификации и программы. Рассмотрим программу со специфи
Отношения порядка
R называется бинарным отношением на множестве D, если R Í D ´ D. Утверждение (a, b) Î R принято записывать в виде a R b. Для произвольного отношения R используются следующ
Наименьшая неподвижная точка
Далее будем считать, что (D, ⊑, ⊥) – полная решетка с наименьшим элементом, т. е. "a Î D. ⊥⊑ a.
Пусть F: D→D - произвольная тотальная (т. е. всюду
Математическая индукция
Математическая индукция – это метод доказательства некоторого утверждения P(n) для всех значений натурального параметра n; n = 0, 1, 2, … . Доказательство проводится по следующей схеме.
Его логическая и операционная семантика
Нас интересуют языки программирования, допускающие построение логической семантики. Во-первых, следует исключить из рассмотрения языки для реактивных систем, определяющих взаимодействующие параллел
Структура программы на языке CCP
Язык CCP (Calculus of Computable Predicates) - язык исчисления вычислимых предикатов, определяющий множество вычислимых формул исчисления предикатов. К языку предъявляются два требования: по
Система типов данных
Любая переменная характеризуется некоторым типом. Язык CCP является бестиповым в том смысле, что типы переменных не указываются в программе, однако их можно однозначно определить по программе. Сист
Логическая и операционная семантика языка CCP
Логическая семантика есть функция LS, сопоставляющая каждой конструкции S языка CCP некоторую формулу LS в исчислении предикатов, т. е. LS(S) = LS. Пусть j(d:
Семантика вызова предиката
Пусть имеется вызов предиката
A(z:u) . (4.12)
Здесь A есть имя предиката или имя переменной предикатного типа; z - возможно пустой набор имен переменных; u - непу
Конструктор предиката
Конструктор предиката является базисным предикатом ConsPred(x, B: A), где x - возможно пустой набор переменных; B - имя предиката; A - имя переменной предикатного типа. Значением п
Конструктор массива
Конструктор массива является базисным предикатом ConsArray(x, B: A), где x - возможно пустой набор переменных, B - имя предиката, отличное от ConsPred и ConsArray. Значением переме
Программа
Программа на языке CCP состоит из конечного набора определений предикатов. Для каждого определения правой частью является оператор суперпозиции (4.16), параллельный оператор (4.19) или услов
Рекурсивные определения предикатов
Для определяемых предикатов B и C отношение depend(B, C) обозначает непосредственную зависимость B от C, если в правой части определения B имеется вызов предиката C. Предикат B определяет
Однозначность предикатов
Применимость правил серии L доказательства корректности программы в соответствующих леммах базируется на однозначности операторов, используемых в определениях предикатов. Покажем, что однозначность
Лексемы
Текст программы представлен в виде последовательности строк символов. Переход на новую строку эквивалентен символу «пробел». Программа может содержать комментарии, текст которых считается не принад
Определение предиката
ОПРЕДЕЛЕНИЕ-ПРЕДИКАТА ::= ИМЯ-ПРЕДИКАТА ОПИСАНИЕ-ПРЕДИКАТА
ИМЯ-ПРЕДИКАТА ::= ИДЕНТИФИКАТОР
Значением ОПИСАНИЯ-ПРЕДИКАТА является предикат, обозначаемый именем предиката.
Спецификация предиката
Предикат, используемый в программе, должен иметь определение предиката. Если предикат определяется в другом модуле программы, то предикат может быть представлен своей спецификацией.
СПЕЦИФ
Вызов предиката
Элементарным оператором программы является вызов предиката.
ВЫЗОВ-ПРЕДИКАТА ::= ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ |
ВЫЗОВ-ПРЕДИКАТА-ГИПЕРФУНКЦИИ
ВЫЗОВ-ПРЕДИКАТА-ФУНКЦИИ ::=
Программа
Программа состоит из одного или нескольких модулей. Модуль определяет независимую часть программы.
ОПИСАНИЕ-МОДУЛЯ ::= [ЗАГОЛОВОК-МОДУЛЯ] СПИСОК-ОПИСАНИЙ
ЗАГОЛОВОК-МОДУЛЯ ::=
Объединение массивов
Операндами операции «+» объединения массивов:
ВЫРАЖЕНИЕ-МАССИВ + ВЫРАЖЕНИЕ-МАССИВ
являются выражения, значениями которых являются массивы. Объединяемые массивы до
Формулы
Формулы, используемые в качестве предусловий и постусловий предикатов, есть формулы типизированного исчисления предикатов высших порядков. Подформула, входящая в предусловие или постусловие, может
Процессы
Для большинства программ можно построить спецификацию в виде предусловия и постусловия. Однако не всякую программу можно специфицировать таким образом. Имеется класс программ реального времени, в ч
Императивное расширение
Императивное расширение языка P определяет дополнительные языковые конструкции, возникающие в программе в результате проведения трансформаций предикатной программы (см. введение). Использование эти
Технология предикатного программирования
Типичный способ реализации языка программирования заключается в реализации транслятора с языка программирования на язык команд целевой ЭВМ или на некоторый другой реализованный язык программировани
Подстановка определения предиката на место вызова
Пусть A(x: y) { S } - определение предиката на императивном расширении языка P, а A(e: z) - вызов предиката в теле некоторого другого предиката B. Здесь x, y, z обозначают списки переменных, а e -
Замена хвостовой рекурсии циклом
Подстановка определения нерекурсивного предиката на место вызова является эффективной при наличии в программе одного вызова. Подстановка определения рекурсивного предиката усложняет программу и поэ
Склеивание переменных
Трансформация склеивания переменных есть замена в определении предиката нескольких переменных одной. Трансформация определяет список имен переменных. Переменные из указанного списка переменн
Метод обобщения исходной задачи
Трансформация замены хвостовой рекурсии циклом является весьма эффективной, поскольку устранение рекурсии позволяет провести подстановку определения на место вызова, после чего открывается возможно
Трансформация кодирования структурных объектов
Трансформация кодирования структурных объектов реализует представление используемых в программе структурных типов (списков, деревьев и др.) посредством структур более низкого уровня, таких к
Гиперфункции
Пример 7.2. Допустим, для списка s целых чисел требуется извлечь второй элемент и присвоить переменной e. Список может содержать менее двух элементов. Логическая переменная exist =
Else break
}
}
};
Подставим определения предикатов взятьЧисло и перваяЦифра на место вызовов. Проведем очевидные упрощения.
Сумма(string s, nat
Else break
}
};
Далее, поскольку внутренний цикл в теле предиката Сумма не имеет нормального выхода, можно заменить оператор #2 на break и убрать скобки оператора продолжени
Else break
}
n = n + v
}
}
На четвертом этапе применяется трансформация кодирования строки s вырезкой массива. При этом разные значения списка s представляются вырезками од
Else break
}
n = n + v
}
Можно обнаружить следующий недостаток программы (7.39): если строка s завершается цифрой, то проверка исчерпания строки реализуется
Хотите получать на электронную почту самые свежие новости?
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Новости и инфо для студентов