Консультация перед коллоквиумом по курсу
«Методы формальных спецификаций программ». 27.10.2004
Часть I. Язык RSL.

Задачи 1-го типа

Дано explicit определение функции. Написать implicit-спецификацию функции эквивалентной данной.

value

f : Int ><Int >< Int -> write x read y Int >< Int

f(a,b,c) is if a=b then

(if a+b > c then c else x:=y; a+b end,

b*(if c>0 then c else 0-c end))

else (x, (x:=a+b; a-b)) end

Решение

value

f : Int ><Int >< Int -> write x, y Int >< Int

f(a,b,c) as (d, e)

post if a=b then

(if a+b > c then x=x’ /\ d=c else x=y /\ d=a+b end /\

if c>0 then e=b*c else e=b*(0-c) end)

else (x’=a+b /\ d=x’ /\ e=a-b) end

Задачи 2-го типа

Дать explicit или implicit определение функций (включая слабейшее предусловие), отвечающих требованиям аксиом:

type S, E value create : Unit -> S, add : E >< S -> S, del : E>< Nat >< S -~-> S, get : E >< S -> Nat,

axiom all e : E, s : S :- get( e, create( ) ) is 0, all e1,e2 : E, s : S :- get ( e1, add (e2, s)) is if e1 = e2 then 1+get( e1, s ) else get( e1, s ) end, all e1, e2 : E, n : Nat, s : S :- del( e1, n, add( e2, s )) is if n=0 then add(e2, s ) elsif e1 = e2 then del( e1, n-1, s ) else add(e2, del( e1, n, s ) ) end

Решение

- мультимножество; у функции del есть предусловие – нельзя исключить большее количество элементов данного значения, чем их имеется в мультимножестве

Задача 3-го типа

Доказать, что вторая спецификация является (или не является) уточнением первой.

value

f1 : B >< B -> Bool

f2 : A >< B -> B

axiom

all a1, a2 : A, b : B :-

f1(f2(a1, b), f2(a2, b)) is a1 = a2,

all a : A, b : B :-

f1(f2(a,b), b) is false

_________________________________________________________________________

type

L = A-list, A = Int, S = A-set

value

f1 : B >< B -> Bool

f1(b1, b2) is hd b1 = hd b2,

f2 : A >< B -> B

f2(a, b) is <. a .> ^ b

Решение

Доказываем первую аксиому

all a1, a2 : A, b : B :-

f1(f2(a1, b), f2(a2, b)) is a1 = a2 [[раскрыть кантор]]

f1(f2(a1, b), f2(a2, b)) is a1 = a2 [[раскрыть f1]]

hd f2(a1, b), = hd f2(a2, b) is a1 = a2 [[раскрыть f2]]

hd <. a1 .> ^ b, = hd <. a2 .> ^ b is a1 = a2 [[раскрыть hd]]

a1 = a2 is a1 = a2 [[unigilated]]

true

Доказываем первую аксиому

all a : A, b : B :- f1(f2(a,b), b) is false [[раскрыть кантор]]

f1(f2(a,b), b) is false [[раскрыть f1]]

hd f2(a, b), = hd b is false [[ раскрыть f2]]

hd <. a .> ^ b = hd b is false [[ раскрыть hd]]

a = hd b is false [[есть контрпример]]

false

Ответ – Вторая спецификация не является уточнением первой

Задача 4-го типа

Рассмотреть возможные варианты результатов вычислений в предположении, что все возможные обмены сообщениями произошли

a!(5+a?) || ((x:=(x:=a?;1)) ++ (b!4 || x:=a? || b!6 || a!3 || y:=b?))

Решение

1 - x:=a?;1

a) y:=4

a!(5+a?) || (x:=1 ++ ( x:=a? || b!6 || y:=4))

a!(5+a?) || (x:=1) || x:=a? || b!6 || y:=4

b) y:=6

a!(5+a?) || (x:=1)) ++ (b!4 || x:=a? || y:=6))

a!(5+a?) || x:=1|| b!4 || x:=a? || y:=6

2 - x:=a?

a) y:=4

a!(5+a?) || ((x:=(x:=a?;1)) ++ ( x:=3 || b!6 || y:=4)) -- stop

b) y:=6

a!(5+a?) || ((x:=(x:=a?;1)) ++ (b!4 || x:=3 || y:=6)) -- stop

Всего 4 решения

Задачи 5-го типа

Дано определение вариантного типа:

type Collection == empty | add (Collection <-> head, tail:Collection)

Дать эквивалентное определение без использования вариантных определений.

Решение:

type Collection

value

empty : Collection,

head : Collection >< Collection -~-> Collection,

tail : Collection -~-> Collection

axiom

all c1, c2, c3 : Collection :-

head (c1, add(c2, c3)) is add(c1, c3)