Алгебраические спецификации в Dafny

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


Для начала простой пример. Библиотека с книгами и читателями.

datatype Book = mk_Book;
datatype Reader = mk_Reader;
datatype Library 
    = empty
    | addBook(Book, Library)
    | addReader(Reader, Library)
    | borrow(Book, Reader, Library)
    ;

function isBookKnown(book : Book, lib : Library) : bool
{
    match lib
        case empty => false
        case addBook(b,l) => b == book || isBookKnown(book, l)
        case addReader(r,l) => isBookKnown(book, l)
        case borrow(b, r, l) => isBookKnown(book, l)
}

Тут один целевой тип - Library. У него 4 генератора: empty, addBook, addReader, borrow. Далее мы определяем обсервер isBookKnown. В его теле используется match expression. По сути он перебирает возможные виды параметра lib и при помощи рекурсии дает определение функции isBookKnown. На RSL то же определение выглядело не так похоже на определение функции, а имело бы вид набора аксиом:

scheme LIBRARY = class
  type Book, Reader, Library
  value empty : Library,
        addBook : Book >< Library -> Library,
        addReader : Reader >< Library -> Library,
        borrow : Book >< Reader >< Library -> Library,
        isBookKnown : Book >< Library -> Bool
  axiom forall book, b : Book, r : Reader, l : Library :-
        isBookKnown(book, empty) is false,
        isBookKnown(book, addBook(b,l)) is b = book \/ isBookKnown(book,l),
        isBookKnown(book, addReader(r,l)) is isBookKnown(book, l),
        isBookKnown(book, borrow(b, r, l)) is isBookKnown(book, l)
end

И сразу же познакомимся с первым преимуществом автоматической верификации спецификаций: если мы напишем в match только строчки с empty и addBook, Dafny выдаст сообщение об ошибке (попробуйте!). Это говорит о том, что Dafny помогает автоматически отслеживать недоспецификацию. А вот и второе преимущество: поскольку Dafny пытается автоматически доказывать завершаемость, то она может находить опечатки, приводящие к "зацикливанию": на это

datatype Book = mk_Book;
datatype Reader = mk_Reader;
datatype Library 
    = empty
    | addBook(Book, Library)
    | addReader(Reader, Library)
    | borrow(Book, Reader, Library)
    ;

function isBookKnown(book : Book, lib : Library) : bool
{
    match lib
        case empty => false
        case addBook(b,l) => b == book || isBookKnown(book, l)
        case addReader(r,l) => isBookKnown(book, lib)
        case borrow(b, r, l) => isBookKnown(book, l)
}

Dafny ответит:

cannot prove termination; try supplying a decreases clause

Далее. Мало уметь задавать генераторы и обсерверы. Нужно иметь возможность сформулировать свойства корректности нашей модели (например, safety свойства) и Dafny должна нам помочь в их верификации. Возможно, тем самым она определит проблемы в нашей модели (речь идет о противоречиях). В частности, для того алгебраические спецификации модели и пишутся, чтобы можно было на них доказывать выполнимость сформулированных отдельно свойств корректности. Правда, это не единственная польза от алгебраических спецификаций. Поясню это опять же на примере. Та же библиотека с книжками и читателями (на самом деле мы еще практически ничего существенного и не описали в нашей модели про библиотеку). Какие возможны свойства корректности:

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

и много еще других свойств корректности (приведите их сами). В этом списке представлены свойства корректности различных видов:

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

Мы остановимся пока на инвариантных свойствах. Для примера рассмотрим такое свойство: "Если книга не находится в библиотеке, то она находится у одного из читателей" (иными словами, книга либо в библиотеке, либо у читателя - библиотека точно знает, где она, и знает, что книга не потерялась). Сформулируем это свойство формально:

forall library, book :: isBookKnown(book, library) ==> (! in_library(book, library) ==> exists reader :: has_book(book, reader, library))

У нас появились новые функции: in_library и has_book. Определим их (это обсерверы):

datatype Book = mk_Book;
datatype Reader = mk_Reader;
datatype Library 
    = empty
    | addBook(Book, Library)
    | addReader(Reader, Library)
    | borrow(Book, Reader, Library)
    ;

function isBookKnown(book : Book, lib : Library) : bool
{
    match lib
        case empty => false
        case addBook(b,l) => b == book || isBookKnown(book, l)
        case addReader(r,l) => isBookKnown(book, l)
        case borrow(b, r, l) => isBookKnown(book, l)
}

function in_library(book : Book, lib : Library) : bool
{
    match lib
       case empty => false
       case borrow(b, r, l) => if b == book then false else in_library(book, l)
       case addReader(r, l) => in_library(book, l)
       case addBook(b, l) => if b == book then true else in_library(book, l)
}

function has_book(book : Book, reader : Reader, lib : Library) : bool
{
    match lib
       case empty => false
       case borrow(b, r, l) => if b == book && r == reader then true else has_book(book, reader, l)
       case addReader(r, l) => has_book(book, reader, l)
       case addBook(b, l) => has_book(book, reader, l)
}

И, наконец, допишем наше свойство в виде "теоремы" (т.е. ghost method) :

ghost method Theorem()
  ensures forall library : Library, book : Book :: 
(   isBookKnown(book, library) ==>
     ( ! in_library(book, library) ==> 
            (exists reader :: has_book(book, reader, library))) );
{
}

Спрашиваем Dafny ... и ...

Dafny program verifier finished with 5 verified, 0 errors

Ура! Нам не потребовалось ничего, кроме умения формально выражать свойства системы! Теперь мы уверены, что если для реализации выполнены определения функций генераторов и обсерверов, то для реализации автоматически будет выполнено свойство корректности! Именно умение абстрагироваться, формальность описаний функций системы и наличие инструмента верификации (Dafny) позволили свести задачу верификации (выяснения, правильна ли) сложной реализации (т.е. выполнено ли свойство корректности) к более простым подзадачам про отдельные операции.