Абстрактные типы данных (АТД)



         

Доказательство достаточной полноты - часть 5


Если у какого-либо подвыражения

u выражения s внешняя функция есть item или empty, то уровень вложенности

u не превосходит n-1, что по предположению индукции позволяет определить корректность u и, если u

корректно, получить его значение, применяя аксиомы. Выполнив замены всех таких подвыражений, получим для s эквивалентную форму, в которую входят только функции put, remove и new.

Далее используем идею введенной выше канонической формы, чтобы избавиться от всех вхождений remove, так что результирующая форма для s

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

  • empty (s) корректно и по аксиоме A3 значение этого выражения есть ложь (false);
  • item (s) корректно, так как предусловие not empty (s) для item выполнено; из аксиомы A1 следует, что значение этого выражения равно x.
  • Это завершает доказательство достаточной полноты, так как мы показали справедливость множества правил - правила корректного веса и правила канонического сокращения, позволяющего нам выяснять корректность заданного стекового выражения, а для корректного выражения-запроса - определять его значение в терминах значений типов BOOLEAN и

    G.




    Содержание  Назад  Вперед