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

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

Это сообщение посвящено стилям написания аксиом для алгебраических спецификаций. Согласно синтаксису аксиома имеет следующий вид: 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

Источники незамкнутости алгебраической спецификации

Среди различных характеристик алгебраических спецификаций можно выделить следующие три важные характеристики:

• полнота

• непротиворечивость

• замкнутость

Полнота означает, что спецификация содержит описание всех нужных свойств. Непротиворечивость означает, что спецификация реализуема, существует программная система, обладающая всеми свойствами, перечисленными в спецификации. Замкнутость означает, что для каждой функциональной особенности (определенные данные, определенные ситуации) есть функция, которая создает эту функциональную особенность.

Эти характеристики нужны при проведении валидации спецификации. Это сообщение посвящено тому, как проверять спецификацию на замкнутость.

Собственно, надо проверить

1. возможность создания целевого типа

2. возможность обнаружения изменений, которые выполняют функции-генераторы;

3. возможность создания ситуаций, в которых функции-обсерверы ведут себя по-разному.

Проверка возможности создания целевого типа

Сначала на примере спецификации с единственным целевым типом. Надо проверить, что есть константа целевого типа или функция-генератор, среди входных параметров которой нет целевого типа. Если спецификация содержит несколько целевых типов, то для каждого целевого типа должна существовать цепочка из констант и функций-генераторов, для которой выполняются все следующие свойства:

1. цепочка начинается с константы;

2. цепочка заканчивается функцией, возвращающей этот целевой тип;

3. каждая следующая функция в цепочка в качестве своего входного параметра принимает целевой тип, возвращаемый предыдущей функцией.

Пример незамкнутой спецификации:

scheme SCHEME = class

type E, S

value

add : E >< S -> S,

remove : E >< S -~-> S

end

Ее можно исправить, например, добавив константу (empty) :

scheme SCHEME = class

type E, S

value empty : S,

add : E >< S -> S,

remove : E >< S -~-> S

end

Проверка возможности обнаружения изменений, выполняемых генераторами

Каждая функция-генератор выполняет некоторую модификацию целевого типа. Функций-обсерверов должно быть достаточно, чтобы "увидеть" выполненные модификации.

Что надо делать:

1. сформулировать свойства (функциональные особенности), которые изменяются после выполнения функции-генератора;

2. проверить, что это изменение отражено в аксиомах;

3. если не отражено, то добавить функции-обсерверы, показывающие эти свойства, и записать недостающие аксиомы.

Пример незамкнутой спецификации:

scheme SCHEME = class

type E, S

value empty : S,

add : E >< S -> S,

remove : E >< S -~-> S

end

Ее можно исправить, например, добавив обсервер has :

scheme SCHEME = class

type E, S

value empty : S,

add : E >< S -> S,

remove : E >< S -~-> S,

has : E >< S -> Bool

axiom all e : E :-

~has(e, empty),

all e1, e2 : E, s : S :-

has(e2, add(e1, s)) is e1 = e2 \/ has(e2, s)

end

Проверка возможности создания ситуаций, в которых обсерверы ведут себя по-разному


Если функция-генератор является частичной функцией (т.е не является тотальной функцией), то надо выписать все условия, гарантирующие ее выполнение (т.е. предусловие). Предусловие - это обычно конъюнкция некоторых более простых условий. Каждое условие представляется в виде функции-обсервера, возвращающего булевское значение. Т.е. добавив в систему функцию-генератор, у нас появится еще и некоторое количество функций-обсерверов. В этом случае для каждой функции-обсервера должен быть генератор, от которого этот обсервер возвращает true на каких-то данных, и должен быть генератор, от которого этот обсервер  возвратит false на каких-то данных. Подобную проверку нужно делать и для обсерверов, возвращающих другие типы данных. Поскольку обычно в типах данных достаточно много значений, то эти значения делят на классы (эквивалентности) и требуют, чтобы в спецификации было описано свойство обсервера возвращать значения из каждого класса.

Что надо делать:

1. для каждого обсервера разделить значения в возвращаемом им типе на классы эквивалентности (для типа Bool один класс содержит true, другой класс - false; для типа Nat это может быть класс, состоящий только из нуля, и класс, состоящий из всех положительных чисел);

2. проверить, что для каждого класса каждого обсервера есть аксиома с цепочкой генераторов, завершающаяся этим обсервером, в котором значение обсервера принадлежит каждому этому классу;

3. если это не так,

   1. сформулировать поведение системы, при котором значение обсервера попадает в нужный класс;

   2. обозначить это поведение в виде цепочки генераторов;

   3. объявить сигнатуры этих генераторов;

   4. объявить необходимые аксиомы с этими генераторами.

Пример незамкнутой спецификации:

scheme SCHEME = class

type Vertex, Edge = Vertex >< Vertex, Graph

value empty : Graph,

add : Edge >< Graph -~-> Graph,

has : Edge >< Graph -> Bool

axiom all e : Edge :-

~has(e, empty),

all e1, e2 : Edge, g : Graph :-

has(e2, add(e1, g)) is e1 = e2 \/ has(e2, g) pre has(e1, g)

end

add обладает предусловием, что добавляемое ребро не должно быть уже добавлено (все ребра в этом графе уникальны). Но это предусловие неполное, т.к. чтобы добавить ребро, надо быть уверенным в существовании вершин ребра (в противном случае мы можем "ошибиться" при вводе edge и добавить ребро, не проверив его, в результате получим "кривой" граф). Итак, нам нужно еще предусловие, поэтому добавляем обсервер:

scheme SCHEME = class

type Vertex, Edge = Vertex >< Vertex, Graph

value empty : Graph,

add : Edge >< Graph -~-> Graph,

has : Edge >< Graph -> Bool,

hasVertex : Vertex >< Graph -> Bool

axiom all e : Edge :-

~has(e, empty),

all e1, e2 : Edge, g : Graph :-

has(e2, add(e1, g)) is e1 = e2 \/ has(e2, g) pre ~has(e1, g)

end