1

Экзамен по курсу «Формальные спецификации программ. 18.12.2002
Часть I. Язык RSL и тестирование на основе формальных спецификаций»

Задачи и решение

Задачи 1-го типа (номер 1)

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

value

f : Int ><Int >< Int -> write x, 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 x:=c; c else 0-c end))

else (y:=a+b; y, 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

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

if c>0 then x=c; d=b*c else x=x’ /\ d=0-c end)

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

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

value

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

f (a, b) is

local variable v : Int := 0 in

for i in <.a..b.> do

v := v+2*(x:=i;i)

end; (a,b,v+y)

end

Решение

value

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

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

post if a<b then x=x’ /\ (c,d,e)=(a,b,y)

else x=b /\ (c,d,e)=(a,b,(a+b)*(b-a+1)+y)

end

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

value

f : Int ><Int >< Int -> write x, y read z 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 x:=c; c else 0-c end))

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

Решение

value

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

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

post if a=b then

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

if c>0 then x=c; d=b*c else x=x’ /\ d=0-c end)

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

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

value

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

f (a, b) is

local variable v : Int := 0 in

y:= x + z;

for i in <.a..b.> do

v := v+(x:=v;2)*i

end; (a,b,v)

end

Решение

value

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

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

post y=x’+z /\ if a<b then x=x’ /\ (c,d,e)=(a,b,0)

else x= (a+b-1)*(b-a) /\ (c,d,e)=(a,b,(a+b)*(b-a+1))

end

Задачи 2-го типа (номер 2)

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

Решение

- мультимножество

2. Дать явную спецификацию, которая может быть уточнением данной:

type С,A = Nat

value

create: Unit -> C,

add : A >< C -> C,

get : C -~-> A >< C

axiom all e:A, l:C :-

get (add(e,l)) is if (e<0) \/ (l=create()) then (e,l)

else let (a,b)=get(l) in (a,add(e,b)) end

end

Решение

type С-list, A = Nat

value

create: Unit -> C create() is <..>,

add : A >< C -> C

add (a,c) is

if (a<0) then a ^ l

else l ^ a end ,

get : C -~-> A >< C

get (c) is (hd c, tl c)

pre len c > 0

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

type S, E

value

create : Unit -> S,

add2 : S >< E -> S,

add3 : E >< S >< E-> S,

del : S -~-> S,

get : S -~-> E

axiom

all e1,e2 : E, s : S :-

del( add3( e1, s, e2 ) ) is add2(s, e2) ,

all e : E, s : S :-

del(add2(s,e)) is if s=create() then create() else add2(del(s), e) end,

all e1,e2 : E, s : S:-

get(add3(e1,s,e2)) is e1,

all e : E, s : S :-

get(add2(s, e)) is if s=create() then e else get (s) end

Решение

add2 реализует очередь, add3 добавляет элемент с двух сторон.

Задача 3-го типа (номер 2)

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

value

f1 : A >< L -~ -> L

f2 : A >< L -~ -> L

f3 : L -> Nat

axiom

all a : A, b : L :-

f3(f1(a,b)) is f3(b)+1

pre f3(b) = 1, -- добавлено предусловие

all a : A, b : L :-

f3(f2(a,b)) is 1+f3(b)

pre f3(b) = 1, -- добавлено предусловие

all a: A, b : L :-

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

pre f3(b) = 1

_________________________________________________________________________

type

L = A-list

value

f1 : A >< L -~ -> L

f1(a, b) is <. a .> ^ tl b

pre b ~= <..>,

f2 : A >< L -~ -> L

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

pre b ~= <..>

f3 : L -> Nat

f3(l) is len l

Решение

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

all a: A, b : L :-

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

pre f3(b) = 1

[[раскрыть кантор]]

if f3(b) = 1 then f1(a,b) is f2(a,b) else true end

[[раскрыть f3,f1,f2]]

if len b = 1 then <. a .> ^ tl b is tl b ^ <. a .> else true end

[[вычислить tl при len b = 1]]

if len b = 1 then <. a .> ^ <..> is <..> ^ <. a .> else true end

[[вычислить ^]]

if len b = 1 then <. a .> is <. a .> else true end

[[вычислить is]]

if len b = 1 then true else true end

[[вычислить if]]

true

Ответ – «Да, является уточнением»

Задача 4-го типа (номер 3)

3. Упростить выражение

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 решения

3. Упростить выражение

(x:=(a? |^| b?)) || ((x:=(if true |^| false then b!1;1 else x:=a?;6 end)) ++ (b!4 || a!3 || y:=b?))

1 – true

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

a) y:= 1

(x:=(a? |^| b?)) || ((x:=1) ++ (b!4 || a!3 || y:=1))

(x:=(a? |^| b?)) || ((x:=1) || (b!4 || a!3 || y:=1))

Result: (x:=3 || b!4 || y:=1 ) |^| (x:=4 || a!3 || y:=1)

b) y:=4

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

2 - false

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

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

Result: x:=a?|| x:=6 || b!4 || y:=b? -- or y:=4

|^| x:=4 || x:=6 || y:=b?

|^| x:=b? || x:=6 || y:=4

Всего 6 решений
3. Упростить выражение

case (a? |^| b?) of

0,1 -> x:=a?+1,

2 -> x:=b? ,

3 -> y:=a?+3,

4 -> y:=b?+a?,

end || a!(b?) || a!0 || b!(a?+4)

Решение

1 – case a?

a) b!(a?+4)

case a? of

0,1 -> x:=a?+1,

2 -> x:=b? ,

3 -> y:=a?+3,

4 -> y:=b?+a?,

end || a!(b?) || b!4 ----> a!4 ---->

Result: y:=b?+a?

b) case

Result: x:=a?+1 || a!(b?) || b!(a?+4)

2 – case b?

a) a!b?

Result: case b? of

0,1 -> x:=a?+1,

2 -> x:=b? ,

3 -> y:=a?+3,

4 -> y:=b?+a?,

end || a!4

b) case

Result: y:=b?+a?|| a!(b?)

3. Упростить выражение

case (a?) of

0,1 -> x:=a?+1,

2 -> x:=b? |^| a?,

3 -> y:=a?+3,

4 -> y:=b?+a?,

end || a!0 || b!(a?) || (a!2 |^| a!3)

Решение

1 – a!2

a) a!2 -> a?

Result: x:=b? --> x:=0

Result: x:=a? --> x:=0 || b!(a?) |^|

x:=a? || b!0

b) a!0->a?

Result: x:=b? |^| a? --> x:=0 |^|

(x:=b? || a!0)

2 – a!3

a) a!0->b!(a?)

Result: y:=a?+3 --> ( y:=3 || b!( a?)) |^|

(y:=a?+3 || b!0)

b) a!3->b!(a?)

Result: x:=a?+1 --> (x:=4 || b!(a?)) |^|

(x:=a?+1 || b!3)

Задача 5-го типа (номер 3 или 4)

4. Определить классы эквивалентности в пространстве входных значений функции f, отвечающие разбиению пространства в соответствии с критерием полноты тестового покрытия “все достижимые дизъюнкты”

variable a, b : Int ...

post

if a+b = 5 /\ (b>4)then ...

elsif (a > b) then ...

else ...

end

pre a+b<=6 \/ a-b>3

Решение

	m1 a+b<=6	m2 a-b>3	m3 a+b = 5	m4 (b>4)	m5 (a > b)	a	b
1	true		true	true		0	5
1	false	true	true	true
2	true		false		true	3	1
2	false	true	true	false	true
2	true		true	false	true	3	2
2	false	true	false		true	6	1
3	true		false		false	2	4
3	false	true	true	false	false
3	true		true	false	false	2	3
3	false	true	false		false

3. Определить классы эквивалентности в пространстве входных значений функции f, отвечающие разбиению пространства в соответствии с критерием полноты тестового покрытия “все достижимые дизъюнкты”

variable a : Int, b : Int –m-> Int

post

if ~((a+1) isin rng b) then ...

elsif (card rng b < card dom b) /\ (b(a) = a) then ...

else ...

end

pre (a isin dom b) \/ b = [ ]

Решение

	m1 a+1 isin dom b	m2 b = [ ]	m3 ~((a+1) isin rng b)	m4 card rng b < card dom b	m5 b(a) = a	A	b
1	true		true			1	[1+>1]
1	false	true	true			1	[]
2	true		false	true	true	1	[1+>1,2+>1,2+>2]
2	false	true	false	true	true
3	true		false	false		1	[2+>2]
3	false	true	false	true	false
3	true		false	true	false	1	[2+>2,3+>2]
3	false	true	false	false

variable a, b : Int ...

post

if (b < 4) then ...

elsif (a + b = 5) \/ (b > 4) \/ (a > b) then ...

else ...

end

pre a+b<=6

Решение

	m1 a+b<=6	m2 b<4	m3 a+b = 5	m4 b>4	m5 a > b	a	b
1	true	true				0	3
2	true	false	true			0	5
2	true	false	false	true		1	5
2	true	false	false	false	true
3	true	false	false	false	false	2	4

variable a : Int, b : Int-list ...

post

if ((a+1) ~isin inds b) then ...

elsif (len b > card elems b) /\ (b(a) = a) then ...

else ...

end

pre (a isin inds b) /\ ( b(a) < 0 )

	m1 (a isin inds b)	m2 b(a) < 0	m3 ((a+1)~ isin inds b)	m4 len b > card elems b	m5 b(a) = a	a	b
1	true	true	true			1	<.0-2.>
2	true	true	false	true	true	1
3	true	true	false	false		1	<.0-2, 1.>
3	true	true	false	true	false	1	<.0-2,0-2.>

Задачи 6-го типа (номер 4)

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

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

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

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

type Collection == empty | add1 (head:Elem) | add2(head : Elem <->head), Elem

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