Бертран Мейер - Основы объектно-ориентированного программирования

Понятие инварианта класса пришло из Хоаровской работы [Hoare 1972a] по инвариантам типов данных. Смотри также приложения к проектированию программ в [Jones 1980], [Jones 1986]. Формальная теория морфизмов между АТД типами может быть найдена у [Goguen 1978].

Библиографические ссылки по формальным языкам спецификаций, включая Z, VDM, OBJ-2, Larch, можно найти в лекции 6. В работе [Lano 1994] , содержащей большое число ссылок, описаны ОО-формальные языки спецификаций, включая Object Z, Z++, MooZ, OOZE, SmallVDM, VDM++.

Стандарты по терминологии программных ошибок, дефектов, неисправностей опубликованы IEEE Computer Society [IEEE 1990], [IEEE1993]. Их Web-страница - http://www.computer.org

Удивительно, но немногие языки программирования поддерживают синтаксическую поддержку утверждений. Ранним примером (первым, который стал мне известен) был язык AlgolW, созданный Хоаром и Виртом [Hoare 1966], непосредственный предшественник языка Pascal. Другие включают Alphard [Shaw 1981] и Euclid [Lampson 1977], спроектированные специально для разработки корректных программ. Связь с ОО-разработкой и нотация, введенная в этой книге, навеяна утверждениями языка CLU [Liskov 1981], который никогда не был реализован. Другая, базирующаяся на CLU книга Лискова и Гуттага [Liskov 1986] является одной из немногих книг по методологии программирования, в которой глубоко обсуждаются вопросы разработки надежного ПО, предлагая подход на базе "защитного программирования", подвергнутый критике в данной лекции.

Понятие Программирования по контракту, представленное в этой лекции и разрабатываемое в оставшейся части книги, пришло из [M 1987a], продолженное в работах [M 1988], [M1989c], [M 1992a]. В работе [M 1994a] обсуждаются толерантный и требовательный подходы к проектированию предусловий, обращая особое внимание на применение этих подходов к проектированию повторно используемых библиотек, включая политику "требовательной любви". Дальнейший вклад в развитие этих идей был сделан Джеймсом Мак-Кимом [McKim 1995], [McKim 1996], [McKim 1996a], а также [Henderson-Sellers], который занимался исследованием позиции поставщика ПО.

Напишите спецификацию АТД для класса COMPLEX , описывающую понятие комплексных чисел с арифметическими операциями. Исходите из точной арифметики.

Проверьте все предусловия и аксиомы АТД STACK , введенного в предыдущих лекциях, и покажите, отображаются ли они в классе STACK4 , а если да, то как.

Покажите, что введение закрытой функции body , возвращающей тело стека, сделает возможным утверждениям класса STACK полностью отражать спецификацию соответствующего АТД. Обсудите теоретическую и практическую значимость такого подхода.

Почему capacity экспортируется для реализации стеков ограниченных размеров, класс STACK2 ?

Напишите инвариант реализации для класса STACK3 .

Обсудите использование функций в утверждениях, в частности, введение функции correct_index в предусловия программ put и item . Если добавить эту функцию в класс ARRAY , то какой статус экспорта следует ей дать?

Покажите, что каждая из четырех попыток бинарного поиска, объявленная как "ошибочная", действительно некорректна. ( Подсказка: в отличие от доказательства корректности, для доказательства некорректности достаточно предъявить один пример, на котором алгоритм приводит к неверному результату: не завершается, выполняет запрещенную операцию, такую, как выход индекса за допустимые границы, любое другое нарушение предусловия).

В этой лекции было показано, что нарушение предусловия указывает на ошибку клиента, а нарушение постусловия указывает на ошибку поставщика. Объясните, почему нарушение инварианта также указывает на ошибку поставщика.

Напишите класс, реализующий алгоритм получения псевдослучайных чисел, основанный на последовательности: n i= f(n i - 1) , где функция f задана, а начальное значение n 0 определяется клиентом класса. Функция не должна иметь побочных эффектов. Определение функции f можно найти в учебниках, таких как [Knuth 1981] и в библиотеках по численным методам.