Простое практическое задание

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

За первую часть можно получить до 10 баллов. За вторую часть можно получить до 20 баллов.

Ниже приводятся формулировки каждой из частей задания. В придачу к ним на семиаре вы получите свой вариант задания.

Каждая из частей задания независима от другой части. Каждую из них необходимо выполнить в соответствующее занятие и сдать в конце него.

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

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

Примечание: методы класса Stage1Tests нужны для того, чтобы вы могли проверить правильность контракта у статического метода самостоятельно. Если вы не успеваеете написать их все до окончания занятия, ничего страшного. Однако чем больше методов вы успели написать, тем больше сможете найти ошибок в своих спецификациях и исправить их до окончания срока выполнения задания.

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

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

Примечание: методы класса Stage2Tests нужны для того, чтобы вы могли проверить правильность спецификации класса самостоятельно.

Последнее изменение: суббота, 23 ноября 2013, 14:00