Пример второй части

Формулировка второй части задания

  1. создайте файл Фамилия_группа_2.java, подставив свою фамилию и номер группы (например, Ivanov_525_2.java).
  2. напишите там публичный класс Фамилия_группа_2, содержащий указанное ниже содержимое.
  3. дополните класс наиболее строгим инвариантом. Инвариант называется наиболее строгим, если из него следует любой другой инвариант класса.
  4. снабдите методы класса контрактами, точно повторяющими указанные ниже требования
  5. напишите в файле Фамилия_группа_2.java непубличный класс Stage2Tests с указанным ниже содержимым.
  6. проверьте, что инструмент Krakatoa успешно доказывает корректность методов класса Stage2Tests относительно написанной вами спецификации класса Фамилия_группа_2. Исправьте найденные ошибки. Обратите внимание, что набор тестовых методов неполный. Они могут помочь найти часть, но не все ошибки в вашей спецификации.

Вариант

class Gamer21 {
    int count;
    int[] previous;
    int index;
    int cancels;

    public Gamer21();
    public int step(int current);
    public boolean isWin();
    public boolean isLose();
}

Требования:
Напишите спецификацию класса Gamer21, реализующего одну из стратегий игрока в игре “21*” согласно указанным ниже требованиям. Спецификация должна содержать наиболее строгий инвариант класса (это такой инвариант класса, из которого следует любой другой инвариант класса), методы класса должны содержать контракт, точно передающий требования, указанные ниже.

Цель игры - набрать ровно 21 очко. Игрок бросает кубик несколько раз и суммирует выпавшие очки. Если в результате он получил в сумме ровно 21, он выиграл. Если же получил больше 21, проиграл. Кубик бросается до тех пор, пока в сумме не наберется хотя бы 21. Игрок может отказаться от очередного выпавшего на кубике числа в пользу одного из очков, выпавших в одном из трех предыдущих ходов, но такое можно делать не более двух раз за игру. Игрок пользуется обычным кубиком, на гранях которого написаны числа от 1 до 6 включительно. На ребро кубик не становится.
Состояние объекта класса Gamer21 состоит из целого числа count - текущей суммы баллов, набранных игроком, массива чисел previous, содержащего 3 предыдущих значения, выпавших на кубике, и целого числа cancels, означающего количество совершенных отказов.

Конструктор инициализирует новую игру. Он обнуляет count, cancels и index и выделяет память под массив previous из 3х элементов, обнуляя их.
Метод step(current) осуществляет ход игрока, если на кубике выпало число current. Метод возвращает целое число, означающее выбор игрока. Если возвращается число 0, значит игрок принял выпавшие очки на кубике. Если возвращает число от 1 до 6, игрок отказался от выпавшего на кубике и заменяет его на возвращаемое значение (оно должно быть в previous). В любом случае сумма очков игрока увеличивается на возвращаемое значение, если оно не 0, и на current, иначе; cancels увеличивается на 1, если возвращается не 0, иначе не меняется. Если cancels был меньше 2, элемент массива previous по индексу index становится равным current (остальные элементы не меняются) и index увеличивается на 1 по модулю размера previous. Если возвращается не 0 (игрок отказывается от выпавших очков), cancels должен увеличиться на 1. Отказываться нельзя, если уже до этого игрок отказался 2 раза. Метод step не должен вызываться, если игра уже окончена (т.е. игрок набрал не менее 21).
Метод isWin возвращает истину тогда и только тогда, когда игра окончена и игрок победил (он набрал 21 очко).
Метод isLose возвращает истину тогда и только тогда, когда игра окончена и игрок проиграл (он набрал больше 21 очка).

Тестовые методы:
class Stage2Tests {
    /*@ requires gamer != null && gamer.count < 3; */
    public static void test01(Gamer21 gamer) {
        if (gamer.step(1) != 0 && gamer.step(1) != 0 && gamer.step(1) != 0) {
            //@ assert false;
        }
    }

    /*@ requires gamer != null; */
    public static void test02(Gamer21 gamer) {
        if (gamer.isWin() && gamer.isLose()) {
            //@ assert false;
        }
    }

    /*@ requires gamer != null; */
    public static void test03(Gamer21 gamer) {
        int c = gamer.count;
        if (c < 21 && gamer.step(3) == 0) {
            if (gamer.isWin()) {
                //@ assert c == 18;
            } else {
                //@ assert c != 18;
            }
        }
    }
}

Решение

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

Последнее изменение: вторник, 26 ноября 2013, 01:55