Е.А. Кузьменкова, А.К. Петренко - Формальная спецификация программ на языке RSL (1158800), страница 8

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 8)

p ^ 1 ^ p(n  1) (i  1)  p(n  1) (i)  i in 2 .. n  1 ^ 1

end

end

1. scheme

PAGE 

class

type Page  Line^*, Line  Word^*, Word

value

is_on : Word  Page  Bool

is_on(w, p)  ( i : Nat • i  inds p  w  elems p(i)),

number_of : Word  Page  Nat

number_of(w, p) 

card {(i, j)  i, j : Nat • i  inds p  j  inds p(i)  w  p(i)(j)}

end

5.1. scheme

MAP_UNIVERSITY_SYSTEM =

class

type

Student,

Course,

CourseInfos = Course m Student-set,

University = Student-set  CourseInfos

value

allStudents : University  Student-set

allStudents(ss, cis)  ss,

hasCourse : Course  University  Bool

hasCourse(c, (ss, cis))  c  dom cis,

numberOK : University  Bool

numberOK(ss, cis) 

( c : Course • c  dom cis 

(card cis(c)  100  card cis(c)  5)),

studOf : Course  University  Student-set

studOf(c, (ss, cis))  cis(c) pre hasCourse(c, (ss, cis)),

attending : Student  University  Course-set

attending(s, (ss, cis)) 

{c  c : Course • c  dom cis  s  cis(c)}

pre s  allStudents(ss, cis),

newStud : Student  University  University

newStud(s, (ss, cis))  (ss  {s}, cis) pre s  ss,

dropStud : Student  University  University

dropStud(s, (ss, cis)) 

(ss \ {s}, [ c ↦ cis(c) \ {s}  c : Course • c  dom cis ])

pre s  ss

end

Пример варианта письменного экзамена

и его решение

В этом разделе все специальные символы RSL указываются в ASCII представлении.

1. Дана неявная спецификация функции, описать ее в явной форме.

value

f : Nat  Nat  Nat

f(a,b) as c

post

if (exists n : Nat :- is_divisor(a,n) /\ is_divisor(b,n)) then

is_divisor(a,c) /\ is_divisor(b,c) /\

all c1:Nat :- is_divisor(a,c1) /\ is_divisor(b,c1) => (c1<=c)

end,

is_divisor : Nat ><Nat -> Nat

is_divisor(a,b) is

b ~= 0 /\

a > b /\

a - (a / b) * b = a,

f : Nat ><Nat -> Nat

f(a,b) is

if a=b then a

elsif a-b > 0 then f(a-b,b) else f(a,b-a) end

Решение:

value

f : Nat ><Nat -> Nat

f(a,b) is

if a=b then a

elsif a-b > 0 then f(a-b,b) else f(a,b-a) end

2. Доказать, что схема S2 является уточнением схемы S1:

scheme

S1 =

class

type A,B,C

value

f1 : A >< B -> Bool,

f2 : A >< B -~-> C,

f3 : C -~-> A >< B

axiom

all a: A, b: B :-

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

pre f1(a,b) = true

end

scheme

S2 =

class

type A=Int, B=Nat, C=Int

value

f1 : A >< B -> Bool

f1(i,n) is i * i = n,

f2 : A >< B -~-> C

f2(i,n) is i,

f3 : C -~-> A >< B

f3(cc) as (a,b)

post (cc = a) /\ b = (cc * cc)

end

Доказательство:

all a: A, b: B :-

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

pre f1(a,b) = true

all_assumption_inf:

[[ if f1(a,b) = true then f3( f2(a, b)) is (a,b) end ]]

unfold_true:

[[ if f1(a,b) then f3( f2(a, b)) is (a,b) end ]]

unfold_f1:

[[ if a*a = b then f3( f2(a, b)) is (a,b) end ]]

unfold_f2:

[[ if a*a = b then f3( a ) is (a,b) end ]]

unfold_f3:

[[ if a*a = b then (a, a*a))is (a,b) end ]]

if_annihilation:

[[ (a, b)is (a,b) ]]

is_annihilation:

true

3. Дана алгебраическая спецификация группы функций, дать определение необходимых типов данных и явное определение функции get.

scheme

EXAM =

class

type R, Key, Val

value

empty : Unit -> R,

put : R >< Key >< Val -> R,

del : R >< Key >< Val -~-> R,

get: R >< Key -~-> Val-set,

find: R >< Key -> Bool,

axiom

forall r : R, k1, k2 : Key, v1, v2 : Val :-

[find_empty] find (empty(), k1) is false,

[find_put] find (put(r, k1, v1), k1) is true,

[get _put]

get (put(r, k1, v1), k1) is

if find (r, k1) then

get (r, k1) union {v1}

else

{v1}

end,

[del_put_1]

del(put(r, k1, v1), k1, v1) is

if find (r, k1) /\ v1 isin get (r, k1) then

del(r, k1, v1)

else

r

end,

[put_put]

put(put(r, k1, v1), k2, v2) is

if (k1 = k2) /\ (v1 = v2) then

put(r, k1, v1)

else

put(put(r, k2, v2), k1, v1)

end

end

Решение:

type R = Key-m->Val-set, Key, Val

value

get: R >< Key -~-> Val-set

get(r,k) as vs

post

vs = r(k)

pre k isin dom r

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

(b!2) || (y:=a?) || if (x:=1); (a!x); (true |^| false) then a!(b?)

else a!(1+b?) end

Решение:

x:=1; (y:=1) ; (a!2) |^|

x:=1; (y:=1) ; (a!3)

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

post

if (a > 5) /\ (b < 3) then ...

elsif ((a > b) /\ (b=0)) \/ (b<3) then ...

else ...

end

Решение:

Ветвь 1: m1 m2

Ветвь 2: нет

Ветвь 3: m1~m2 m3~m4~m2

m1 ~m2 ~m3~m2

~m1 m3 ~m4

~m1~m3 m2

~m1 m3 ~m4 m2

~m1 m3 ~m4 ~m2

~m1 ~m3 ~m2

Пояснение. Затененные клетки таблицы указывают на несовместимые условия.

Дополнительные примеры заданий с решениями.

Темы.

1. Определение классов эквивалентности для AFDNF критерия полноты тестового покрытия по неявным спецификациям.

2. Упрощение параллельных и недетерминированных выражений.

Тема: Определение классов эквивалентности для AFDNF критерия полноты тестового покрытия по неявным спецификациям.

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

1. value

f : Int >< Int-list >< Nat -~-> Nat >< Bool

f (a,b,c) as (q,p)

post

if (a + len b > c) /\ (a isin elems b) then ...

elsif (a>=c) /\ (a isin inds b) then ...

else …

end

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

2. post

if (a > 4) /\ (b < 4) then ...

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

else ...

end

pre b<= 4

Решение:

post

if m2 /\ m3 then ...

elsif m4 /\ m5 then ...

else ...

end

pre m1

B1 – m1m2m3

Характеристики

Список файлов книги