Полезное:
Как сделать разговор полезным и приятным
Как сделать объемную звезду своими руками
Как сделать то, что делать не хочется?
Как сделать погремушку
Как сделать так чтобы женщины сами знакомились с вами
Как сделать идею коммерческой
Как сделать хорошую растяжку ног?
Как сделать наш разум здоровым?
Как сделать, чтобы люди обманывали меньше
Вопрос 4. Как сделать так, чтобы вас уважали и ценили?
Как сделать лучше себе и другим людям
Как сделать свидание интересным?
Категории:
АрхитектураАстрономияБиологияГеографияГеологияИнформатикаИскусствоИсторияКулинарияКультураМаркетингМатематикаМедицинаМенеджментОхрана трудаПравоПроизводствоПсихологияРелигияСоциологияСпортТехникаФизикаФилософияХимияЭкологияЭкономикаЭлектроника
Библиографические замечания. Из работы Тони Хоара [Hoare 1981]:
|
|
Из работы Тони Хоара [Hoare 1981]:
| Первым защитником использования утверждений в программировании был никто иной, как сам Алан Тьюринг. На конференции в Кембридже 24 июня 1950 г. он представил небольшой доклад "Проверка больших программ", в которой объяснял эту идею с большой ясностью. "Как можно проверить большую программу, утверждая, что она правильна? Чтобы для проверяющего задача не была слишком трудной, программист обязан написать некоторые утверждения, которые можно проверить индивидуально, и из которых корректность программы следует достаточно просто." |
Понятие утверждения, представленное в этой лекции, восходит к работам по корректности программ, пионерами которых были Боб Флойд [Floyd 1967], Тони Хоар [Hoare 1969], Эдсгар Дейкстра [Dijkstra 1976], в дальнейшем описанные в [Gries 1981]. Книга "Введение в теорию языков программирования" (Introduction to the Theory of Programming Languages) [M 1990] представляет обзор этого направления.
Понятие инварианта класса пришло из Хоаровской работы [Hoare 1972a] по инвариантам типов данных. Смотри также приложения к проектированию программ в [Jones 1980], [Jones 1986]. Формальная теория морфизмов между АТД типами может быть найдена у [Goguen 1978].
Библиографические ссылки по формальным языкам спецификаций, включая Z, VDM, OBJ-2, Larch, можно найти в Ошибка! Недопустимый объект гиперссылки.. В работе [Lano 1994], содержащей большое число ссылок, описаны ОО-формальные языки спецификаций, включая Object Z, Z++, MooZ, OOZE, SmallVDM, VDM++.
Стандарты по терминологии программных ошибок, дефектов, неисправностей опубликованы IEEE Computer Society [IEEE 1990], [IEEE1993]. Их Web-страница - Ошибка! Недопустимый объект гиперссылки.
Удивительно, но немногие языки программирования поддерживают синтаксическую поддержку утверждений. Ранним примером (первым, который стал мне известен) был язык 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], который занимался исследованием позиции поставщика ПО.
Date: 2015-12-13; view: 484; Нарушение авторских прав