- •Замок дракона
- •Надёжное программное средство как продукт технологии программирования. Исторический и социальный контекст программирования
- •Программа как формализованное описание процесса обработки данных.
- •Программное средство
- •Неконструктивность понятия правильной программы
- •1.3. Надежность программного средства
- •Технология программирования как технология разработки надежных программных средств
- •Технология программирования и информатизация общества
- •Литература
- •Замок дракона
- •Источники ошибок в программных средствах
- •Интеллектуальные возможности человека
- •Неправильный перевод как причина ошибок в программных средствах
- •Модель перевода
- •Основные пути борьбы с ошибками
- •Жизненный цикл программного средства
- •Понятие качества программного средства
- •Обеспечение надёжности — основной мотив разработки программных средств
- •Методы борьбы со сложностью
- •Обеспечение точности перевода
- •Преодоление барьера между пользователем и разработчиком
- •Контроль принимаемых решений
- •Литература
- •Замок дракона
- •Внешнее описание программного средства
- •Назначение внешнего описания программного средства и его роль в обеспечении качества программного средства
- •Определение требований к программному средству
- •Спецификация качества программного средства
- •Функциональная спецификация программного средства
- •Методы контроля внешнего описания программного средства
- •Литература
- •Замок дракона
- •Л. Витгенштейн
- •Методы спецификации семантики функций
- •Основные подходы к спецификации семантики функций
- •Метод таблиц решений
- •Операционная семантика
- •Денотационная семантика
- •Аксиоматическая семантика
- •Аксиоматическая семантика
- •Литература
- •Замок дракона
- •Архитектура программного средства
- •Понятие архитектуры программного средства
- •Основные классы архитектур программных средств
- •Архитектурные функции
- •Контроль архитектуры программных средств
- •Литература
- •Замок дракона
- •Разработка структуры программы и модульное программирование
- •Цель модульного программирования
- •Основные характеристики программного модуля
- •Методы разработки структуры программы
- •Контроль структуры программы
- •Литература
- •Лекция 8. Разработка программного модуля
- •8.1. Порядок разработки программного модуля.
- •8.2. Структурное программирование.
- •8.3. Пошаговая детализация и понятие о псевдокоде.
- •8.4. Контроль программного модуля.
- •Литература к лекции 8.
- •Лекция 9. Доказательство свойств программ
- •9.1. Обоснования программ. Формализация свойств программ.
- •9.2. Свойства простых операторов.
- •9.3. Свойства основных конструкций структурного программирования.
- •9.4. Завершимость выполнения программы.
- •9.5. Пример доказательства свойства программы.
- •Литература к лекции 9.
- •Лекция 10. Тестирование и отладка программного средства
- •10.1. Основные понятия.
- •10.2. Принципы и виды отладки.
- •10.3. Заповеди отладки.
- •10.4. Автономная отладка модуля.
- •10.5. Комплексная отладка программного средства.
- •Литература к лекции 10.
- •Лекция 11. Обеспечение функциональности и надежности программного средства
- •11.1. Функциональность и надежность как обязательные критерии качества программного средства.
- •11.2. Обеспечение завершенности программного средства.
- •11.3. Обеспечение точности программного средства.
- •11.4. Обеспечение автономности программного средства.
- •11.5. Обеспечение устойчивости программного средства.
- •11.6. Обеспечение защищенности программных средств.
- •Литература к лекции 11.
- •Лекция 12. Обеспечение качества программного средства
- •12.1. Общая характеристика процесса обеспечения качества программного средства.
- •12.3. Обеспечение эффективности программного средства.
- •Литература к лекции 12.
- •Лекция 13. Документирование программных средств
- •13.1. Документация, создаваемая в процессе разработки программных средств.
- •13.2. Пользовательская документация программных средств.
- •Литература к лекции 13.
- •Лекция 14. Аттестация программного средства
- •14.1. Назначение аттестации программного средства.
- •14.2. Виды испытаний программного средства.
- •14.3. Методы оценки качества программного средства.
- •Лекция 15.Оъектный подход к разработке программных средств
- •15.1. Объекты и отношения в программировании. Сущность объектного подхода к разработке программных средств.
- •15.2. Объекты и субъекты в программировании.
- •15.3. Объектный и субъектный подходы к разработке программных средств.
- •15.4. Объектный подход к разработке внешнего описания и архитектуры программного средства.
- •Литература к лекции 15.
Денотационная семантика
В денотационной семантике алгебраического подхода рассматривается также система равенств вида (0), которая интерпретируется как система функциональных уравнений, а определяемые функции являются некоторым решением этой системы. В классической математике изучению функциональных уравнений (в частности, интегральных уравнений) уделяется большое внимание и связано с построением достаточно глубокого математического аппарата. Применительно к программированию этими вопросами серьезно занимался Д. Скотт [45].
Основные идеи денотационной семантики проиллюстрируем на более простом случае, когда система равенств (5.3) является системой языковых уравнений:
X1 = φ1,1 φ1,2 ... φ1,k1,
X2 = φ2,1 φ2,2 ... φ2,k2,
(0) .....…………………………
Xn= φn,1 φn,2 ... φn,kn,
причем i-ое уравнение при ki = 0 имеет вид
Xi =
Как известно, формальный язык — это множество цепочек в некотором алфавите. Такую систему можно рассматривать как одну из интерпретаций набора правил некоторой грамматики, представленную в форме Бэкуса-Наура (каждое из приведенных уравнений является аналогом некоторой такой формулы). Пусть фиксирован некоторый алфавит A = {a1, a2, …, am} терминальных символов грамматики, из которых строятся цепочки, образующие используемые в системе (0) языки. Символы X1, X2, ..., Xn являются метапеременными грамматики, здесь будут рассматриваться как переменные, значениями которых являются языки (множества значений этих метапеременных). Символы φi,j, i = 1, ..., n, j = 1, ..., kj, обозначают цепочки в объединенном алфавите терминальных символов и метапеременных:
φi,j (A | { X1, X2, ..., Xn})* .
Цепочка φi,j рассматривается как некоторое выражение, определяющее значение, являющееся языком (множеством цепочек в алфавите A). Такое выражение определяется следующим образом. Если значения X1, X2, ..., Xn заданы, то цепочка
φ = Z1 Z2 ... Zk, Zi(A | { X1, X2, ..., Xn }),
обозначает сцепление множеств Z1 Z2 ... Zk, причём вхождение в эту цепочку символа aj представляет множество из одного элемента {aj}. Это означает, что φ определяет множество цепочек
{ p1 p2 ... pk | pjZj, j = 1, ..., k},
причём цепочка
p1, p2, ..., pk
представляет собой последовательность выписанных друг за другом цепочек p1, p2, ..., pk. Таким образом, каждая правая часть уравнений системы (0) представляет собой объединение множеств цепочек.
Решением системы (0) является набор значений (языков)
L1, L2, ..., Ln
переменных X1, X2, ..., Xn, для которых все уравнения системы (0) превращаются в тождество.
Рассмотрим в качестве примера частный случай системы (0), состоящий из одного уравнения
X = a X b X c
с алфавитом A = {a, b, c}. Решением этого уравнения является язык
L = { φ c | φ{a, b}*}.
Система (0) может иметь несколько решений. Так в рассмотренном примере помимо L решениями являются также
L1 = L {φ a | φ{a, b}*}
и
L2 = L { φ b | φ{a, b}*}.
В соответствии с денотационной семантикой в качестве определяемого решения системы (0) принимается наименьшее. Решение (L1, L2, ..., Ln) системы (0) называется наименьшим, если для любого другого решения (L′1, L′2, ..., L′n) выполняется
L1 L′1, L2 L′2, ..., Ln L′n.
Так в рассмотренном примере наименьшим (а значит, определяемым денотационной семантикой) является решение L.
В качестве метода решения систем уравнений (0) и (0) можно использовать метод последовательных приближений. Сущность этого метода для системы (0) заключается в следующем. Обозначим правые части уравнений системы (0) операторами Ti(X1, X2, ..., Xn). Тогда система (0) примет вид
X1 = T1(X1, X2, ..., Xn),
X2 = T2(X1, X2, ..., Xn),
(0) ………………………
Xn = Tn(X1, X2, ..., Xn).
В качестве начального приближения решения этой системы примем набор языков (L1[0], ..., Ln[0]) = (, , ..., ). Каждое следующее приближение определяется по формуле:
(L1[0], ..., Ln[0]) = (T1(L1[i–1], ..., Ln[i–1]), …………….. (Tn(L1[i–1], ..., Ln[i–1])).
Так как операции объединения и сцепления множеств являются монотонными функциями относительно отношения порядка Н, то этот процесс сходится к решению (L1, ..., Ln) системы (0), т.е.
(L1, ..., Ln)= (T1(L1, ..., Ln), ..., Tn(L1, ..., Ln))
и это решение является наименьшим. Это решение называют ещё наименьшей неподвижной точкой системы операторов
T1, T2, ..., Tn.
В рассмотренном примере этот процесс даёт следующую последовательность приближений:
L[0] = , L[1] = {c}, L[2]= {c, ac, bc},
L[3] = {c, ac, bc, aac, abc, bac, bbc},
…………………………………………
Этот процесс сходится к указанному выше наименьшему решению L.