end

Очевидно, аксиома (условие корректности) не выполнена, т.к. при reg1(m) = reg2(m) < 2 выполнены одновременно lamp_on(m) и lamp_blink(m). Мы обнаружили ошибку в реализации и показали это при помощи формальных методов. Исправим:

value lamp_blink : Machine -> Bool

lamp_blink(m) is reg1(m) < 20 /\ reg1(m) >= 2

А14. Для данной неявной спецификации ответить на вопрос, определяет ли она однозначно возвращаемый результат. Ответ обосновать.

Пример:
value find : Nat-list >< Nat -~-> Nat
find(xs, x) as k
post k isin inds xs /\ xs(k) >= x /\ xs(k) < 2*x

Ответ: неоднозначно.

Пример: find(<. 1, 1, 1, 1 .>, 1) может вернуть любое число от 1 до 4.

А15. Опишите на естественном языке из каких частей будет состоять контракт приведенного ниже метода на языке Java и какие свойства будут составлять каждую из частей.

Пример:

class java.io.InputStream

public abstract int read() throws IOException

Reads the next byte of data from the input stream. The value byte is returned as an int in the range 0 to 255. If no byte is available because the end of the stream has been reached, the value -1 is returned. This method blocks until input data is available, the end of the stream is detected, or an exception is thrown. A subclass must provide an implementation of this method.

Returns: the next byte of data, or -1 if the end of the stream is reached.

Throws: IOException - if an I/O error occurs.

Ответ с консультации:

1) предусловие: -

2) постусловия:

• возвращаемое значение - текущий байт потока, если он доступен, -1 в противном случае

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

• возвращаемое значение - число от -1 до 255.

3) побочный эффект - изменение системных данных, отвечающих за поток

4) возникновение исключительных ситуаций - IOException при возникновении ошибки ввода/вывода.

Рецепт:

В объектно-ориентированном программировании контракт метода обычно включает следующую информацию:

• возможные типы входных данных и их значение (предусловие);

• типы возвращаемых данных и их значение( постусловие) ;

• условия возникновения исключений, их типы и значения;

• присутствие побочного эффекта метода;

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

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

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

• (иногда) гарантии производительности, например, временная сложность или сложность по памяти.

А16. Задание на понятие абстракции.

Пример: Ваша команда разрабатывает модуль почтового веб-клиента для автоматизации работы с контактами корпоративной почты. Модуль нужен для упрощения выбора адресатов писем и ведения списка писем. Опишите на RSL необходимую и достаточную абстракцию почтового веб-клиента (набор сигнатур и сортов) для разработки и исследования модуля. Прокомментируйте на естественном языке семантику введенных вами имён функций и типов данных.

Ответ(с консультации):

type Mail, Address

value recv_mail: Mail -~-> Mail >< Address-set

Почтовый клиент получает почту и передает нам адресаты из писем.

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

А17. Вопрос по теме «Formal Testing».

Пример: Достаточно ли для выполнения критерия MC/DC обеспечить покрытие всех конъюнктов в СДНФ разложении постусловия функции и почему?

Ответ (из лекций-презентаций|это не ответ, это скорее то, из чего надо вывести ответ):

Для обеспечения полного покрытия по этому методу необходимо выполнение следующих условий:

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

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

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

Рецепт: молиться, чтобы этого не было на экзамене.

А18. Вопрос по теме «UniTESK».

Пример: приведите не менее двух критериев полноты на основе программных контрактов.

Предположение:

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

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

Источник: http://panda.ispras.ru/~kuliamin/lectures-mbt/Lecture08.pdf

Рецепт: молиться, чтобы этого не было на экзамене.

«Теоретические» задания

Б1. Дать определение термина в одном-двух предложениях. Определение должно пояснять смысл термина.

Пример: предусловие операции.

Ответ: Условие на входные данные операции, состояние исполняющего операцию объекта, и состояние среды, в которой находится объект, которое должен обеспечить тот, кто вызвал операцию.

Рецепт: Ботать Термин

Б2. Привести одно отличие двух данных понятий.

Пример: VDM и RAISE.

Ответ: в RAISE нельзя менять выбранное уточнение типов. в VDM можно.

Методы Флойда

«Практические» задания

А1. Для данных пред- (pre) и пост- (post) условия, записанных на RSL, предложите реализацию функции P, которая является частично корректной относительно них. Для записи функции так же используйте RSL. Функция должна завершаться на максимальном числе входных данных, удовлетворяющих предусловию. Функция P должна быть представлена в явном виде (в частности, без неявных конструкций таких как кванторы, неявный let, сокращенные (comprehended) выражения), без использования бесконечных значений целых чисел, бесконечных множеств, chaos и т. п.). Функция P должна быть корректно определена (в частности, все частично определенные операции, например, hd, должны вызываться только для тех аргументов, на которых они определены).

Пример:
pre(x, y) = hd x > hd y
post(x, y, z) = z(2) isin elems tl tl x

Ответ: прошу проверить.

value f : Int-list >< Int-list -~-> Int-list

f(x, y) is if len x <= 2 then f(x, y) else <. 1 hd tl tl x .> end

pre len x > 0 /\ len y = 0 0 --> /\ hd x > hd y hd y? Павел Батанов: я думаю предусловаия должны быть написаны, а постусловиям функция должна удовлетворять. -->

А2. В блок-схеме программы выделена подсхема, в которую входит ровно одна дуга и из которой выходит ровно одна дуга. Известно, что про эту схему доказана полная корректность относительно некоторых пред- и пост- условий. При этом дуге, ведущей в подсхему, была сопоставлена точка сечения A и оценочная функция uА, а дуге, исходящей из подсхемы, точка сечения В и оценочная функция uВ. Фундированное множество обозначено как W. Для данных uА, uВ, W предложить содержимое подсхемы (в виде программы на RSL) и утверждение в точке А, гарантирующее достижимость В из А на максимальном числе данных. x - входная переменная программы, y1, y2 - промежуточные переменные.

Пример:
uA = len y1 + len y2
uB = uA
W = (Nat, <)

Ответ: проверьте

подсхема: if y2 != <..> then y2 := tl y2 else y1 := tl y1 end;

утверждение в точке А: y1 ^ y2 != <..>

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

Пример: блок-схема содержит 2 вложенных цикла

Ответ: 1. точка сечения в начале внутреннего цикла. Нуля недостаточно, т.к. тогда все циклы будут без точек сечения..

Рецепт: Не должно быть возможности зациклиться без прохождения точки сечения.

А4. Что из перечисленного может быть индуктивным утверждением? (все свободные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: а,в,д

Рецепт: Индуктивные утверждения - это булевы функции от переменных

А5. Что из перечисленного может быть оценочной функцией ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: а,б,в,д

Рецепт: Все что является функцией (булевы функции тоже сойдут)

А6. Что из перечисленного может быть фундированным множеством ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: г

Рецепт: Это множество + операция (по фэншую - частично упорядоченное множество). Если операция <, то множество должно быть ограниченно снизу, > - сверху. В множестве не должно существовать последовательности, которая монотонно убывает(возрастает), но НЕ делает это за конечное число шагов. Т.о, мн-во рац. чисел не годится (можно бесконечно убывать), целые тоже, а вот натуральные вполне сгодятся.

А7. Что из перечисленного может быть условием корректности ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: в

Рецепт: Условия корректности определения оценочной функции: all x in Dx, all y in Dy [ qi(x, y) ⇒ ui(x, y) in W ]

А8. Что из перечисленного может быть условием верификации ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 /\ true => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: в

Рецепт: условия верификации: all x in Dx, all y in Dy [ pi(x, y) /\ R(x, y) ⇒ pj( x, r(x, y) ) ]

А9. Что из перечисленного может быть условием завершимости ? (все указанные переменные целочисленные, эквивалентные преобразования формул не производились, за исключением, быть может, опускания несущественных скобок)

Пример:
а) t > 0
б) t
в) all t : Int :- (t > 0 => t+1 > 0)
г) (Nat U { -2 }, < )
д) all y : Int :- exists t : Int :- (y > t => t > 0)

Ответ: Ничего

Рецепт: условия завершимости: all x in Dx all y in Dy [ qi(x, y) /\ R(x, y) ⇒ ( ui(x,y) > uj(x, r(x, y) ) ) ]. Оценочная функция должна убывать

А10. Сколько необходимо операторов языка блок-схем для записи модели следующей функции языка Си ? Ответ обосновать. Что делает эта функция?

Пример:

int P(int x) {
int y1 = x, y2 = 0;
if (x < 0) {
return 0;
} else {
while (y1 > y2) {
y1--; y2++;
}
return y1;
}
}

Ответ: START, TEST, HALT, JOIN, TEST, ASSIGN, HALT = 7 операторов

Ф-ция вычисляет x/2.

Рецепт: Нарисовать граф функции как для Флойда. Посчитать блоки

А11. Каково минимальное и максимальное число утверждений, которые необходимо доказать при использовании лишь одной точки сечения в рамках доказательства частичной корректности заданной функции P (она задана на языке Си) ? Ответ обосновать. Если одной точки сечения недостаточно, обосновать это.

Пример:

int P(int x) {
int y1 = x, y2 = x;
do {
if (y1 > y2 + y2) {
y2 ++;
}
y1 += y2;
} while (y1 < y2);
return y1 + y2;
}