Ключевые концепции

• Теория абстрактных типов данных (АТД) примиряет необходимость в точности и полноте спецификаций с желанием избежать лишних деталей в спецификации.
• Спецификация абстрактного типа данных является формальным математическим описанием, а не текстом программы. Она аппликативна, т.е. не включает в явном виде изменений.
• АТД может быть родовым, и он задается функциями, аксиомами и предусловиями. Аксиомы и предусловия выражают семантику данного типа и важны для полного и однозначного его описания.
• Частичные функции образуют удобную математическую модель для описания не всюду определенных операций. У каждой частичной функции имеется предусловие, задающее условие, при котором она будет выдавать результат для заданного конкретного аргумента.
• ОО-система - это совокупность классов. Каждый класс основан на некотором абстрактном типе данных и задает частичную или полную реализацию этого АТД.
• Класс является эффективным, если он полностью реализован, в противном случае он называется отложенным.
• Классы должны разрабатываться в наиболее общем виде, допускающем повторное использование; процесс их объединения в систему часто идет снизу-вверх.
• Абстрактные типы данных являются скорее неявными, чем явными описаниями. Эта неявность, которая также означает открытость, переносится на весь ОО-метод.
• Не существует формального определения интуитивно ясного понятия "полноты" спецификации абстрактного типа данных. Строго определяемое понятие достаточной полноты как правило обеспечивает удовлетворительный ответ. Хотя не существует метода, устанавливающего достаточную полноту произвольной спецификации, часто удается ее доказать для конкретных спецификаций; приведенное в этой лекции доказательство достаточной полноты для спецификации стеков может служить образцом и для других случаев.

Дата добавления: 2014-01-03