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

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

• полнота
• непротиворечивость
• замкнутость

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

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

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

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

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

scheme SCHEME = class
    type Vertex, Edge = Vertex >< Vertex, Graph
    value empty : Graph,
          add : Edge >< Graph -~-> Graph, 
          has : Edge >< Graph -> Bool,
          hasVertex : Vertex >< Graph -> Bool,
          addVertex : Vertex >< Graph -~-> Graph,
          v1 : Edge -> Vertex v1((v,_)) is v,
          v2 : Edge -> Vertex v2((_,v)) is v
    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)
              /\ hasVertex(v1(e), g)
              /\ hasVertex(v2(e), g),
          all e: Edge, v: Vertex, g : Graph :-
             has(e, addVertex(v, g)) is has(e, g) 
             pre ~hasVertex(v, g),

          all v : Vertex :-
             ~hasVertex(v, empty),
          all v1, v2 : Vertex, g : Graph :-
             hasVertex(v1, addVertex(v2, g)) is v1 = v2 \/ hasVertex(v1, g)
             pre ~hasVertex(v2, g),
          all v: Vertex, e: Edge, g : Graph :-
             hasVertex(v, add(e, g)) is hasVertex(v, g)
             pre ~has(e, g)
              /\ hasVertex(v1(e), g)
              /\ hasVertex(v2(e), g)
end