Алгебраические аксиомы без предусловий

Это сообщение посвящено стилям написания аксиом для алгебраических спецификаций. Согласно синтаксису аксиома имеет следующий вид: all var : type :- bool_expr [pre bool_expr] (предусловие необязательно). А алгебраическая аксиома имеет вид: all var : type :- expr is expr [pre bool_expr] , где оба expr - это функциональные термы, предусловие необязательно. Идея алгебраического способа записи свойств состоит в том, чтобы всякие хитрые кванторы и логические связи выразить только при помощи композиций операций системы. Предусловие - по сути тоже использует логическую связку (импликацию), поэтому можно было бы пытаться выражать аксиомы без нее, т.е. без предусловий. Посмотрим, во что это выливается, как при этом меняется способ формулирования аксиом.



Начнем с несложного примера. Есть библиотека, в которой есть книжки и читатели:

scheme LIBRARY = class
    type Book, Reader, LibDB
    value empty: LibDB,
             addBook : Book >< LibDB -~-> LibDB,
             knownBook : Book >< LibDB -> Bool,
             addReader : Reader >< LibDB -~-> LibDB,
             knownReader : Reader >< LibDB -> Bool,
             borrow : Book >< Reader >< LibDB -~-> LibDB,
             return : Book >< Reader >< LibDB -~-> LibDB, 
             hasBooks: Reader >< LibDB -~-> Bool, 
             removeReader : Reader >< LibDB -~-> LibDB
     axiom all b : Book :-
                   knownBook(b, empty) is false,
              all b : Book, lib : LibDB :-
                   knownBook(b, addBook(b, lib)) is true
                        pre ~knownBook(b, lib),
              all b, b' : Book, lib : LibDB :-
                   knownBook(b', addBook(b, lib)) is false
                        pre b ~= b' /\ ~knownBook(b, lib),
              .....              all r : Reader, lib : LibDB :-
                   knownReader(r, removeReader(r, lib)) is false
                           pre knownReader(r, lib)
                             /\ ~hasBooks(r, lib)
               ...........
end

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

По сути надо что-то написать вместо lib, чтобы для этого lib были выполнены оба условия (knownReader и не-hasBooks). Т.е. если сначала добавляется читатель, то его можно удалять сразу же. Если добавляется читатель и он берет книгу, то он сначала возвращает книгу и тогда может быть удален. Смотрите: мы начинаем задумываться о цепочках операций (и ведь мы тем самым думаем о композициях операций, что ближе к стилистике алгебраических спецификаций). Итак, получается следующие аксиомы:

all r : Reader :-
          knownReader(r,
                  removeReader(r,
                           addReader(r,
                                  empty))) is false,
all r : Reader, b : Book :-
          knownReader(r,
              removeReader(r,
                     return(b, r,
                            borrow(b, r,
                                    addReader(r,
                                        empty))) is false,

Функции остались частичными, но они вызываются в аксиомах тогда, когда их "предусловия" выполнены. Обратите внимание, что стиль написания "с предусловиями" очень напоминает программный контракт, а представленные только что цепочки операций - это явно не контракт. А что же тогда? Это сценарии работы с программной системой, не вдающиеся в детали реализации, но тем не менее описывающие отделяющие правильные системы от неправильных (правильные - те, на которых все свойства выполнены). Они крайне похожи на unit-тесты! Одна аксиома - один тест.

Итак, это можно использовать, например, для записи функциональности в виде тестов. Знаете про ТDD ? Test-Driven Development.

Возникает ряд вопросов:

1. что лучше - с предусловиями или без них;
2. как понять, полна ли такая алгебраическая спецификация (полон ли набор тестов)
3. помогает ли какой-либо из стилей (с предусловиями / без предусловий) более качественным спецификациям в результате.

На счет первого вопроса ответ должен следовать из цели, для которой пишется спецификация. Если бы речь шла про RAISE с его пошаговым уточнением от абстрактного описания интерфейса к описании реализации, то спецификации с предусловиями и "короткими аксиомами" (один обсервер + один генератор) легко трансформируются в модель на пред- и пост- условиях (для этого достаточно сохранить предусловие и в качестве постусловия записать конъюнкцию равенств обсервера от результата операции правой части аксиомы с этим обсервером). Но при этом надо либо сразу писать аксиомы с предусловиями, либо заниматься преобразованием аксиом без предусловий в аксиомы с предусловиями, т.е. пытаться "сократить" цепочки генераторов в аксиомах до одного генератора.

С другой стороны в ряде случаем нужные предусловия для аксиом неочевидны или заведома общее предусловие на первых этапах спецификации может помешать доказательству наличия уточнения между этой, абстрактной, спецификацией и некоторой другой, более конкретной, спецификацией (например, если бы мы забыли указать свойство не-hasBooks, а написали бы только очевидное knownReader). Если же мы пишем только цепочки операций, то мы точно не сделаем этой ошибки. Кроме того, сразу получим модульные тесты! (кстати, если у нас есть программный контракт, то мы можем получить основу для проведения model-based testing, тестирования на модели, но для ее организации необходимо привлекать сторонние инструменты, например, SpecExplorer или инструменты семейства UniTESK).

Вполне очевидно, что оценить полноту спецификаций по набору модульных тестов непросто, только если есть какая-нибудь систематика множества состояний (ветви функциональности операций), множества входных воздействий, множества внешних эффектов операций. Всё это проще отследить, имея программный контракт. Однако "алгебра" может служить "более легким" (lightweight) способом спецификации, в которой полнота не является доминирующим фактором.

Над третьим вопросом предлагается читателю подумать самостоятельно.

Напоследок небольшое замечание технического характера. В первой спецификации в этой заметке есть аксиома с двумя книгами: b и b', которые должны быть разными. Поскольку это свойство книг не имеет никакого отношения к системе (оно не содержит в себе lib), то, кажется, аксиому с ним нельзя преобразовать в вид "без предусловия". Действительно, так и есть. В этом случае разрешается в правой части аксиомы указать несколько функциональных термов внутри условного оператора if-then-else. Пример:

all r, r' : Reader :-
          knownReader(r',
                  removeReader(r,
                      addReader(r', 
                           addReader(r,
                                  empty)))) is
           if r = r' then false else true end