Вопросы и ответ к экзамену по курсу «Формальная спецификация и верификация программ» янв. 2013

ВНИМАНИЕ: В связи со случаями вандализма доступ на редактирование ограничен!

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

http://img541.imageshack.us/img541/9292/20130123145453.jpg

http://img138.imageshack.us/img138/5917/20130123145504.jpg

RSL и RAISE метод

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

А1. По данной явной спецификации построить эквивалентную неявную спецификацию без использования рекурсии и циклов.

Пример:
variable x : Int, y : Int
value f : Unit -~-> write x, y Nat
f() is (if x + y > 0 then y := x end;x+y)

Ответ:

variable x : Int, y : Int
value f : Unit -~-> write x, y Nat
f() as n
post x’ = x /\ n = x + y /\
( if x` + y` > 0 then y = x` else y = y` end )

Рецепт:

Выражение id’ обозначает значение переменной id в состоянии до вызова функции.

Не забывать про предыдущие значения (особенно в условных выражениях), не забывать про x = x’ во всех ветках, если он не меняется. (C.Павел)

(А. Зачесов) Сюда добавлю еще три задачи, которые были в лекциях. Задание точно такое же:

А1.1
variable x : Int
value f : Int-list -~-> write any Nat
f(xs) is local variable c : Nat := 0 in
for i in <. 1 .. len xs.> do
if xs(i) = x then c := c+1 end
end;
c
end

Ответ:

Эта функция выдает количество вхождений числа x в список xs.

f(xs) as cnt

post (xs = xs’) /\ (x = x’) /\ (cnt = card {n | n : Nat :- (n isin inds xs) /\ (xs(n) = x)})

A1.2

variable x : Int
value f : Unit -~-> write any Nat-set
f() is local variable ps : Nat-set := {} in

for p in <.2 .. x-1.> do

if exists k : Nat :- k isin ps /\ p\k = 0
then skip
else ps := ps union {p} end;

end;

ps

end

Ответ:

Выдает множество всех простых чисел меньше x.

value f:Unit -~-> Nat-set

f() as ps

pre x > 2

post forall p : Int :- ( p >= 2 /\ p < x /\ ( exists k:Nat :- k >= 2 /\ p\k = 0) ) p ~isin ps= 2 /\ p = 2 /\ k

post forall p : Int :- ( p >= 2 /\ p < x /\ ( exists k:Nat :- k >= 2 /\ p\k ~= 0) ) p isin ps

A1.3

variable x : Int
value f : Unit -~-> write any Nat-list
f() is local variable s : Nat-list := <..>, k : Int := 0, i : Int := 1 in
while i <= x do
k := k + 2*i + 1;
i := i + 1;
s := s ^ <.k.>
end;
s
end

Ответ:

Выдает список с числами n*(n+2) для всех натуральных n <= x.

value f:Unit -~-> Nat-list

f() as s

post forall p : Int :- ( p > 0 /\ p <= x ) p*(p+2) isin elems(s)

post forall p : Int :- ( p > 0 /\ p <= x-1 ) s(p) < s(p+1)

А2. По данной неявной спецификации функции f построить явную спецификацию этой функции, являющуюся уточнением данной неявной спецификации.

Пример:
value f : Nat-list >< Nat -~-> Nat
f(nums, max) as n
post n < len nums /\ sum(nums, n) < max /\ sum(nums, n+1) >= max
pre max > 0 /\ max <= sum(nums, len nums)
value sum : Nat-list >< Nat -> Nat
sum(s, n) is if n = 0 then 0 else hd s + sum(tl s, n-1)
pre n <= len s

Ответ:

value f : Nat-list >< Nat -~-> Nat
f(nums, max) is ff(nums, 0, max)
value ff : Nat-list >< Nat >< Nat -~-> Nat
ff(nums, partsum, max) is if partsum + hd nums >= max then 0 else ff(tl nums, partsum + hd nums, max) + 1 end

pre max > 0 /\ max <= sum(nums, len nums)

Альтернативный ответ:

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

f(nums, max) is if hd nums >= max then 0

else 1 + f(tl nums, max - hd nums)

end

pre max > 0 /\ max <= sum(nums, len nums)

Рецепт:

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

• реализация сохраняет объявления всех сущностей исходной спецификации (абстрактные типы могут заменяться описанием типа, подтипы могут заменяться своими максимальными типами),

• могут появляться объявления и описания новых сущностей и свойств,

• все свойства (аксиомы) исходной спецификации остаются справедливыми в реализации.

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

Функция sum(s, n) возвращает сумму первых n элементов списка s. Функция sum описана в явном виде. Функция f(nums, max) возвращает максимальное число первых элементов списка, сумма которых меньше max.

А3. По данной алгебраической спецификации вычислить значение выражения, если это возможно сделать. В ответе представить процесс вычисления в виде переписывания термов.

Пример: выражение: first(add(add(add(add(add(empty, 5), 100), 0), 2), 20)).
Алгебраическая спецификация:
scheme A0 = class
type S
value empty : S,
add : S >< Nat -> S,
first : S -~-> Nat
axiom all s : S, e : Nat :-
first(add(s, e)) is if e > 10 then 2 * first(s)
elsif e > 5 then first(s)
else 0 end
end

Ответ: first(add(add(add(add(add(empty, 5), 100), 0), 2), 20)) = 2 * first(add(add(add(add(empty, 5), 100), 0), 2)) = 2 * 0 = 0. Вычисление возможно.

А4. Закончите аксиому алгебраической спецификации типа данных S, формализующую поведение указанных далее операций над этим типом. Пример: S - очередь ограниченного размера capacity, add - добавление в очередь, size - количество элементов в очереди.

scheme QUEUE = class
type S, E
value capacity : Nat
value empty : S,
add : S >< E -~-> S,
size : S -> Nat
axiom all s : S, e : E :- size(add(s, e)) is . . .

Ответ.

axiom all s : S, e : E :- size(add(s, e)) is if size(s) >= capacity then capacity else size(s)+1 end

Альтернативный ответ

axiom all s : S, e : E :- size(add(s, e)) is size(s)+1 pre size < capacity

А5. Указать, какие из стилевых характеристик относятся к данной спецификации (явная, неявная, алгебраическая, моделеориентированная, аппликативная, императивная, формальная, неформальная).

Пример: (в качестве спецификации может быть любой текст, который встретился в курса, а именно RSL-спецификация, PVS-теоремы)

scheme S = class
type T, E
variable x : Nat
end

Ответ: императивная, формальная.

Рецепт: стили спецификаций //lecture-2011-09-28.pdf:

Я так понимаю, что

явная\неявная определяется через использование is в определениях переменных и формул

формальная\неформальная - через используемый язык (неформальная - на естественном языке обычно)

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

А6. Запишите на RSL полный инвариант указанного типа согласно заданию, не меняя определений типов. При необходимости можете добавить новые разделы спецификации. Полный инвариант типа - тот, из которого следуют все возможные инварианты этого типа.

Пример: type E, S = E-list
S является стеком ограниченного размера

Ответ:
value size : Nat
type E, S = E-list
axiom all s : S :- len s <= size

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

Пример:
а) <. x**2 | x in <.1 .. 3.> :- abs x < 10 .>
б) {x, y, x} \ { x }
в) [ 1 +> 2 ] !! [ 1 +> 3 ] union [ 2 +> 2 ]
г) x > 0 /\ x + y < 1 /\ y > 2
д) x isin s => x isin (s union t)

Ответ: а) <.1, 4, 9 .>, б) {y}\{x}, в) [1 +> 3, 2 +> 2], г) false, д) true

Рецепт: быть внимательным, иметь список приоритета операций и знать, что они делают. И думать больше.

А8. Приведите пример инвариантного свойства состояния указанной подсистемы/системы или её объекта (объектов) управления, которое она должна поддерживать (на русском языке).

Пример: диспетчер виртуальной памяти.

Ответ: Не существует двух записей одного и того же вирт адреса, которые ведут на разные физические адреса

А9. Для данной подсистемы/системы привести один пример её операции, которую имеет смысл на ранних этапах формальной спецификации определить частично (т.е. не тотально). Укажите условие, при котором эта операция будет не определена в такой спецификации.

Пример: диспетчер виртуальной памяти

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

А10. Опишите возможное отношение соответствия между двумя моделями заданных видов.

Пример: неявная спецификация и явная спецификация.

Ответ: вводим функцию абстракции и следуем согласно диаграме коммутативности

Источник: ответы, выданные на консультации.

А11. Сформулировать на RSL возможную функцию абстракции от типа Simpl в тип Sspec.

Пример: type A, B, Simpl = A -m-> B, Sspec = (A><B)-set

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

value retr: Simple -> Sspec
retr(m) is {(x,m(x)) | x : A :- x isin dom m}

А12. В процессе уточнения моделей была построена следующая цепочка типов: S1 ~~~> S2 ~~~> S3 (S2 уточняет S1, S3 уточняет S2). Для данных S1 и S3 приведите S2, нетривиально отличающийся от S1 и S3.

Пример: type A, B, C, S1 = (A >< B >< C)-set, S3 = A -m-> (B >< C)

Ответ: type S2=(A >< B) -m-> C

Источник: ответы, выданные на консультации.

Рецепт: нетривильно = появляется новая информация.

А13. Верифицируйте описанную в задании реализацию программной системы. Т.е. кратко сформулируйте формальную модель реализации (поместите его в ответ), формальной сформулируйте требование корректности (поместите его в ответ) и проведите верификацию (в ответ поместите краткое описание, как вы это делали, и вердикт).

Пример: Разрабатывается управляющая микросхема аппарата по размену купюр и монет. Аппарат принимает одну купюру (10р, 50р, 100р) или монету (10р) и выдает монеты достоинством 5р на ту же сумму. У аппарата есть лампочка, которая моргает в том случае, если размен купюры невозможен (например, закончились монеты или обнаружена внутренняя проблема), и горит непрерывно, если невозможен как размер купюры, так и размен монеты. Разработчики решили завести в аппарате 2 регистра. Если у автомата запрашивают размен монеты, то из второго регистра вычитается число 2 и его значение копируется в первый регистр. Если у автомата запрашивают размен купюры, то из первого регистра вычитается 2, 10 или 20 (в зависимости от достоинства купюры) и его значение копируется во второй регистр. Если в первом регистре число меньше 20, лампочка начинает моргать. Если во втором регистре число меньше 2, лампочка переводится в режим постоянного горения.

Ответ:

scheme MONEYS_MACHINE = class

type Machine :: reg1 : Nat, reg2 : Nat

value lamp_blink : Machine -> Bool

lamp_blink(m) is reg1(m) < 20

value lamp_on : Machine -> Bool

lamp_on(m) is reg2(m) < 2

value input_bank : Machine >< Nat -~-> Machine

input_bank(m, n) as m2

post reg1(m2) = reg1(m) - n /\ n isin {2, 10, 20}

value input_money : Machine -~-> Machine

input_money(m) as m2

post reg2(m2) = reg2(m) - 2 /\ reg1(m2) = reg2(m2)

pre ~lamp_on(m)

- лампочка либо только горит, либо только моргает, либо выключена

axiom all m: Machine :- ~lamp_blink(m) \/ ~lamp_on(m)