Этап написания алгебраической спецификации (корректность систем "со скрытым состоянием")

Это сообщение является продолжением сообщения "Для чего нужна часть курса ФСВП о спецификации" и посвящена этапу написания алгебраической спецификации.

Крайне рекомендуется к прочтению всем, кто выполняет этот этап в рамках практического задания по RSL.


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

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

1. определиться с интерфейсом вашей системы, т.е. какие ей можно "посылать команды", какие есть у команды аргументы, есть ли внешняя реакция системы на команду и, если есть, то какая; см. пример с БД в вводной части; никаким иным образом, кроме как посылкой ей команд, с системой взаимодействовать нельзя; не забывать, что система - это черный ящик, у нас нет никакой возможности узнать, что происходит внутри системы, когда мы ей послали команду;
2. выписать интерфейс в виде сигнатур. Если вы хотите писать спецификацию в императивном стиле (почему бы и нет, это даст вам больше ассоциаций с знакомыми и более практичными языками программирования), не забудьте указать у функций write any, если операция может менять состояние, и read any, если не может. Обратите внимание, что типы аргументов операций и внешних эффектов могут быть только "простыми": числами, булевскими значениями, enumeration, строки.  Например, для примера с БД эти сигнатуры могут выглядеть так:
      scheme CleverDB = class
      type Data
      type Status == ok | error
      value start : Unit -> write any Unit,
            insert : Data -> write any Status,
            remove : Data -> write any Status,
            is_it_here : Data -> read any Bool
     end
   В аппликативном стиле спецификация также возможна, хотя и несколько непривычна:
      scheme CleverDB = class
      type DB, Data
      type Status == ok | error
      value start : Unit -> DB,
            insert : DB >< Data -> DB >< Status,
            remove : DB >< Data -> DB >< Status,
            is_it_here : DB >< Data -> Bool
     end
   Учтите, что внешний эффект - это должны быть "осязаемые" вещи: числа, булевские значения, строки (которые представляются при помощи типа Text в RSL), константы, но никак не, например, sort-типы.
3. Теперь можно думать о свойствах сеансов работы. Но для начала стоит сделать отступление, чтобы пояснить, как знание о свойствах превращается в аксиомы. Начнем с простого свойства: после включения системы никаких данных в ней нет. Здесь речь идет о сеансе из двух операций: сначала start, потом is_it_here. Причем вторая должна возвращать всегда false. Записываем это в императивном стиле:
         all d : Data :-
          start( );
          is_it_here(d) = false
   Здесь фигурирует квантор всеобщности, а, например, при реальном тестировании будут некие конкретные данные, конечно.
   Следующее свойство: после включения системы и успешного добавления неких данных в БД проверка на их наличие должна давать истину. Сеанс состоит из трех операций: start, потом insert, потом is_it_here. Записываем:
         all d : Data :- local variable s1 : Status in
          start( );
          s1 := insert(d);
          if s1 == ok then
              is_it_here(d) = true
          else true end
       end
   Следующее свойство: после включения системы и успешного добавления неких данных в БД проверка наличия других данных должна давать ложь. Записываем:
         all d, d' : Data :- local variable s1 : Status in
          start( );
          s1 := insert(d);
          if s1 == ok then
              is_it_here(d') = false
          else true end
       end
       pre d ~= d'
   Тут квантор снабжен предусловием pre d ~= d', значит при реальном тестировании надо будет проверять "черный ящик" только на разных d и d'.
   Рассмотрим более длинный сеанс и свойства наличия или отсутствия данных:
         all d1, d2, ... : Data :-
        local variable s : Status, f : Bool in
          start( );
          s := insert(d1); s == ok => (
          s := remove(d2); s == ok => (
          s := insert(d3); s == ok => (
          s := insert(d4); s == ok => (
          f := is_it_here(d);
          if d = d4 then f = true                  elsif d = d3 then f = true
          elsif d = d2 then f = false
          elsif d = d1 then f = true
            else f = false   end )))) end
   Те же аксиомы можно записать и в аппликативном виде, хотя они могут быть не столь наглядными. Например, свойство отсутствия данных при старте системы в аппликативном виде будет выглядеть так:
         all d : Data :-
                      is_it_here( start( ), d ) = false
   
   Таким же образом можно думать (и нужно думать) о других свойствах системы: остаются ли данные, добавленные ранее, после очередного добавления; добавляются ли некоторые дополнительные данные при очередном добавлении некоторых данных и т.п.
   
   Так можно перечислять лишь сеансы конечной длины, начинающиеся в старте системы. Для описания сеансов произвольной длины и начинающиеся не обязательно при включении системы нужно использовать квантор по состояниям: always. Например, свойство наличия некоторых данных после успешного добавления (перед которым было еще много всего сделано над БД) можно записать так:
   always all d, d' : Data :- local variable s : Status, f1, f2 : Bool in
         f1 := is_it_here(d);
         s := insert(d'); s == ok => (
         f2 := is_it_here(d);
         if d = d' then f2 = true else f2 = f1 end )
     end
   
   Итак, на этом этапе нужно подумать и сформулировать (в голове) свойства системы на основе "сеансов" работы.
   
   Обратите внимание, что у черного ящика нет способа получить внутреннее состояние (например, в какую-нибудь локальную переменную) и сформулировать про него утверждение. В этом смысле аппликативная спецификация мешает этому правильному понимаю и позволяет именовать разные внутренние состояния и их сравнивать. Так вот, поскольку мы работаем в терминах "черного ящика" сравнивать значения, представляющие некие внутренние структуры, запрещается.