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

Всякое правильно построенное и корректное стековое выражение, не содержащее функций-запросов item и empty, имеет эквивалентную каноническую форму, которая не содержит функции remove (т.е. состоит только из функций put и new>). Эта каноническая форма получается путем применения аксиомы стека A2 всегда, пока это возможно.

Таким образом, мы завершили доказательство достаточной полноты, но только для выражений, не содержащих функции-запросы, и, следовательно, только свойства S1 (проверка корректности выражения). Для завершения доказательства нужно рассмотреть выражения, включающие функции-запросы, и обсудить задачу S2 (нахождение значений для выражений-запросов). Это означает, что нам нужно некоторое правило для определения корректности и значения всякого правильно построенного выражения вида f(s), где s - это правильно построенное выражение, а f - это либо item, либо empty.

Это правило и доказательство его корректности также используют индукцию по уровню вложенности. Пусть n - это уровень вложенности s. Если n=0, то s может быть только new, поскольку остальные функции требуют аргументов и, следовательно, содержат хоть одну пару скобок. Тогда для обеих функций-запросов ситуация ясна:

[x].empty (new) корректно и имеет значение истина (true) (по аксиоме A3);

[x].item (new) некорректно, так как предусловие item требует выполнения not empty (s) .

Индукционный шаг: предположим, что s имеет уровень вложенности n не менее 1. Если у какого-либо подвыражения u выражения s внешняя функция есть item или empty, то уровень вложенности u не превосходит n-1, что по предположению индукции позволяет определить корректность u и, если u корректно, получить его значение, применяя аксиомы. Выполнив замены всех таких подвыражений, получим для s эквивалентную форму, в которую входят только функции put, remove и new.

Далее используем идею введенной выше канонической формы, чтобы избавиться от всех вхождений remove, так что результирующая форма для s будет включать только функции put и new. Случай, когда s это просто new уже был рассмотрен, остался случай, когда s имеет вид put(s', x) . В этом случае для двух рассматриваемых выражений имеем:

[x].empty (s) корректно и по аксиоме A3 значение этого выражения есть ложь (false);

[x].item (s) корректно, так как предусловие not empty (s) для item выполнено; из аксиомы A1 следует, что значение этого выражения равно x.

Это завершает доказательство достаточной полноты, так как мы показали справедливость множества правил - правила корректного веса и правила канонического сокращения, позволяющего нам выяснять корректность заданного стекового выражения, а для корректного выражения-запроса - определять его значение в терминах значений типов BOOLEAN и G.

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

[x]. Теория абстрактных типов данных (АТД) примиряет необходимость в точности и полноте спецификаций с желанием избежать лишних деталей в спецификации.

[x]. Спецификация абстрактного типа данных является формальным математическим описанием, а не текстом программы. Она аппликативна, т.е. не включает в явном виде изменений.

[x]. АТД может быть родовым, и он задается функциями, аксиомами и предусловиями. Аксиомы и предусловия выражают семантику данного типа и важны для полного и однозначного его описания.

[x]. Частичные функции образуют удобную математическую модель для описания не всюду определенных операций. У каждой частичной функции имеется предусловие, задающее условие, при котором она будет выдавать результат для заданного конкретного аргумента.

[x]. ОО-система - это совокупность классов. Каждый класс основан на некотором абстрактном типе данных и задает частичную или полную реализацию этого АТД.

[x]. Класс является эффективным, если он полностью реализован, в противном случае он называется отложенным.

[x]. Классы должны разрабатываться в наиболее общем виде, допускающем повторное использование; процесс их объединения в систему часто идет снизу-вверх.

[x]. Абстрактные типы данных являются скорее неявными, чем явными описаниями. Эта неявность, которая также означает открытость, переносится на весь ОО-метод.