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

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

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

Задание по алгебраической спецификации: основные дефекты

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

• осуществляемое отображение (каков будет эффект после применения такой-то функции, возможно, предваренной применением ряда других, подготавливающих, функций);

• ограничения на возможность выполнения операции (предусловия).

Основные дефекты - это

• отсутствие достаточно представительного набора функциональных свойств;

• неполнота (эффект цепочки функций описывается не на всех данных, на которых его можно описать);

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

Проиллюстрирую эти дефекты на примерах.

type Book, Bookinfo, Reader, Readerinfo

value emptyReaders: Unit -> Readerinfo,

addReader: Reader >< Readerinfo -> Readerinfo,

Здесь функция addReader вряд ли может быть тотальной. Она должна быть частичной, т.к. вполне логичным и нужным было бы такое функциональное свойство (или, по-другому, функциональное требование) "Один и тот же читатель может быть зарегистрирован не более одного раза".

value /*проверяет наличие книги у читателя*/

readerHasBook: Reader >< Book -> Bool,

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

axiom [hasBook_delete]

all book: Book, booksInfo: Bookinfo :-

hasBook(book, deleteBook(book, booksInfo)) = false,

Во-первых, неполнота, т.к. описывается цепочка hasBook от deleteBook только при совпадении их первых параметров. Решение: добавление аксиомы hasBook(book, deleteBook(book2, booksInfo)) для любых book и book2 (а раз для любых, то и, в том числе, для разных).

Во-вторых, т.к. функция deleteBook частичная, то надо задуматься, всегда ли её вызов в цепочке hasBook(book, deleteBook(book2, booksInfo)) будет с допустимыми параметрами (допустимые - те, на которых эта функция определена). В этом примере получается, что может deleteBook быть вызвана с недопустимыми аргументами. Решение: добавление предусловия к аксиоме, т.е. нужно ограничить область действия квантора всеобщности по book и book2 только допустимыми значениями. Корректная аксиома может выглядеть так:

axiom [hasBook_delete]

all book, book2: Book, booksInfo: Bookinfo :-

hasBook(book, deleteBook(book2, booksInfo)) is

if book = book2 then false

else hasBook(book, booksInfo) end

pre hasBook(book2, booksInfo)

Пойдем дальше.

axiom all book:Book, readersInfo: Readerinfo :-

if exists reader:Reader :- (hasReader(reader, readersInfo) /\ readerHasBook(reader, book)) then

isBookFree(book, readersInfo) = false

else isBookFree(book, readersInfo) = true end,

Этот дефект называется неалгебраичность аксиомы. Вместо того, чтобы написать аксиомы isBookFree # empty, isBookFree # addBook, isBookFree # addReader и с остальными генераторами, автор спецификации решил написать квантор существования. Кванторы плохи тем, что усложняют доказательство теорем про функции системы. А такими теоремами могут быть какие-нибудь свойства корректности, которые мы должны все доказать. (см. сообщение в блоге про алгебраические спецификации в Dafny).

И это еще не все дефекты, продолжаем.

axiom [canReaderGetBook]

all reader: Reader, book: Book, needToCarryOut: Bool, readersInfo:Readerinfo :-

canReaderGetBook(reader, readersInfo, book, needToCarryOut) =

hasReader(reader, readersInfo) /\

isBookFree(book, readersInfo) /\

(needToCarryOut => canBookBeCarriedOut(book)) /\

canReaderGetOneMoreBook(reader) /\

~readerHasBook(reader, book),

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


И последний, но, пожалуй, один из самых важных дефектов покажу на спецификации другой системы - системы, которая должна организовывать электронное генеалогическое дерево. 

type

PersonInfo = NameType >< DateType >< DateType >< Sex >< AryanPurity,

System,

Id

value emptyBase : System,

addPerson : System >< PersonInfo -> System >< Id,

hasPerson : Id >< System -> Bool,

addChildren : Id >< Id >< System -> System,

findChildrens : Id >< System -~-> Id-set,

axiom [findChildrens_add]

all system : System, id1, id2 : Id :-

let t = card (findChildrens(id1, system)),

s = addChildren(id1, id2, system) in

card (findChildrens(id1, s)) = t + 1

end

pre hasPerson(id1, system) /\ hasPerson(id2, system),

Во-первых, очевидная неполнота. Исправляем:

type

PersonInfo = NameType >< DateType >< DateType >< Sex >< AryanPurity,

System, Id

value emptyBase : System,

addPerson : System >< PersonInfo -> System >< Id,

hasPerson : Id >< System -> Bool,

addChildren : Id >< Id >< System -> System,

findChildrens : Id >< System -~-> Id-set,

axiom [findChildrens_add]

all system : System, id, id1, id2 : Id :-

let t = findChildrens(id1, system),

s = addChildren(id1, id2, system) in

findChildrens(id, s) is

if id = id1 then {id2} union t else t end

end

pre hasPerson(id1, system) /\ hasPerson(id2, system),

addChildren является генератором, findChildrens (кстати, "дети" по-английски будут children, а "ребенок" - child) - обсервером. Значит, их надо корректно описать через другие генераторы и обсерверы. Сейчас же addChildren и findChildrens не фигурируют больше нигде в спецификации, хотя в ней есть другие обсерверы и генераторы. Получается, что можно судить о том, чему равен findChildren, только если перед этим выполнен addChildren. Хотя очевидно, что findChildren можно вычислить всегда. Обнаружен дефект.

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

Итак, дефект состоит в том, что не выделены, не сформулированы важные свойства вида "предусловие операции", проистекающие из предметной области. Как исправить этот дефект? Во-первых, сформулировать все свойства "по-русски". Затем их формализовать: предложить, возможно, дополнительные функции-обсерверы, задать их при помощи аксиом со всеми генераторами и дополнить ими предусловие аксиом, где выполняются частичные операции (типа addChildren).