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

Условие задания

Дан класс, описывающий состояние игры в крестики-нолики, и позволяющий с этим состоянием работать.

public abstract class TickTackToe {
   public static int NONE;
   public static int X;
   public static int O;

   public TickTackToe(int n) { ... }
   public abstract void makeStep(int row, int col);
   public abstract boolean isFinished();
   public abstract int getWinner();
   public abstract int getStepsCount();
}

Требования:

  • игра происходит на поле размера n на n (n -- параметр конструктора), игроки по очереди выставляют крестики и нолики, выигрывает тот, кто выставил вертикаль, горизонталь или диагональ из n символов;

  • первыми ходят крестики;

  • каждый из двух игроков ставит фишки только одного типа;

  • игроки могут ставить крестики и нолики только в свободные места игрового поля;

  • пропускать ход нельзя, ничья бывает только при невозможности сделать ход;

  • игра после выигрыша не продолжается;

  • константа X идентифицирует фишку “крестик”, константа O -- нолик, константа NONE означает отсутствие крестика и нолика;

  • метод makeStep() производит ход по указанным координатам; row означает номер строки, col означает номер колонки; строки и колонки нумеруются с нуля;

  • метод isFinished() возвращает истину тогда и только тогда, когда невозможно сделать очередной ход в игре (т.е. игра закончилась);

  • метод getWinner() возвращает идентификатор фишки выигравшего игрока, если игра закончилась и в игре есть победитель; если игра закончилась вничью, метод возвращает NONE;

  • метод getStepsCount() возвращает количество сделанных ходов с момента начала игры.

Требуется формализовать эти требования.

Этап 1

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

  • поле field хранит поле игры; номер строки должен быть первым индексом этого массива, номер колонки, соответственно, вторым; массив должен быть размера n на n;

  • поле currentPlayer хранит идентификатор фишки игрока, чей ход будет следующим, если игра ещё не закончилась, или был бы следующим, если бы игра не закончилась.

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

Этап 2

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

public TickTackToe(int n) {

     //@ ghost this.n = n;
     //@ ghost field = new int[n][];

     for(int i = 0; i < n; i++) {
           //@ ghost field[i] = new int[n];

           for(int j = 0; j < n; j++) {
                 //@ ghost field[i][j] = NONE;
           }
      }

      //@ ghost currentPlayer = X;

}

Мы выписали инварианты и варианты циклов, а также некоторые дополнительные утверждения (assert'ы). Кроме того, ряд утверждений был сформулирован отдельно в виде лемм для упрощения доказательства кода. Леммы при этом, конечно, необходимо доказать. Результат нашей работы можно скачать здесь. В этом файле имеется доказательство некоторых лемм (доказательство остальных лемм делается аналогично). Корректность реализации относительно спецификации в этом примере доказывается при помощи солверов Z3, CVC3 и CVC4.

Обратите внимание на размер кода! Прочтите его целиком и представьте, какой объем новой информации вам потребуется изучить для выполнения сложного практического задания. Добейтесь того, чтобы это решение второго этапа действительно доказывалось. Для этого внесите исправления в Krakatoa, запустите его и доказывайте утверждения, выбирая подходящий солвер. Обратите внимание на то, что для доказательства некоторых утверждений их необходимо разбить на части (кнопкой Split) или подставить в них определения функций (кнопкой Inline). Если у вас не получится это сделать, подумайте, насколько вы готовы выполнять сложное практическое задание.

Патч от 10 ноября

Из-за наличия бага в версии Krakatoa, распространяемой в виртуальной машине и расположенной на сайте krakatoa.lri.fr, невозможно показать правильность выполнения этапа 2 без исправления этого бага. Чтобы его исправить, нужно собрать Krakatoa, заменив соответствующие файлы:

  • jc/jc_constructors.mli
  • java/java_interp.ml
  • lib/why3/jessie3theories.why

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

Вы можете задавать вопросы Евгению Корныхину (kornevgen@cmc.msu.ru) или Денису Буздалову.

Последнее изменение: суббота, 11 апреля 2015, 00:50