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

len k〉〉илиrev : Elem* → Elem*rev(k) ≡case k of〈〉 → 〈〉,〈i〉 ^ lr → rev(lr) ^ 〈hd k〉end4.2.type N1 = {| n : Nat • n ≥ 1 |}valuepascal : N1 → (N1*)*pascal(n) ≡if n = 1 then 〈〈1〉〉elselet p = pascal(n − 1) inp ^ 〈〈1〉 ^ 〈p(n − 1) (i − 1) + p(n − 1) (i) | i in 〈2 .. n − 1〉〉 ^ 〈1〉〉endend474.3.schemePAGE =classtype Page = Line*, Line = Word*, Wordvalueis_on : Word × Page → Boolis_on(w, p) ≡ (∃ i : Nat • i ∈ inds p ∧ w ∈ elems p(i)),number_of : Word × Page → Natnumber_of(w, p) ≡card {(i, j) | i, j : Nat • i ∈ inds p ∧ j ∈ inds p(i) ∧ w = p(i)(j)}end5.1.schemeMAP_UNIVERSITY_SYSTEM =classtypeStudent,Course,CourseInfos = Course −m→ Student-set,University = Student-set × CourseInfosvalueallStudents : University → Student-setallStudents(ss, cis) ≡ ss,hasCourse : Course × University → BoolhasCourse(c, (ss, cis)) ≡ c ∈ dom cis,numberOK : University → BoolnumberOK(ss, cis) ≡(∀ c : Course • c ∈ dom cis ⇒(card cis(c) ≤ 100 ∧ card cis(c) ≥ 5)),studOf : Course × University −∼→ Student-setstudOf(c, (ss, cis)) ≡ cis(c) pre hasCourse(c, (ss, cis)),attending : Student × University −∼→ Course-setattending(s, (ss, cis)) ≡{c | c : Course • c ∈ dom cis ∧ s ∈ cis(c)}pre s ∈ allStudents(ss, cis),newStud : Student × University −∼→ UniversitynewStud(s, (ss, cis)) ≡ (ss ∪ {s}, cis) pre s ∉ ss,dropStud : Student × University −∼→ UniversitydropStud(s, (ss, cis)) ≡(ss \ {s}, [ c ↦ cis(c) \ {s} | c : Course • c ∈ dom cis ])pre s ∈ ssend48Пример варианта письменного экзаменаи его решениеВ этом разделе все специальные символы RSL указываются в ASCIIпредставлении.1.

Дана неявная спецификация функции, описать ее в явной форме.valuef : Nat × Nat → Natf(a,b) as cpostif (exists n : Nat :- is_divisor(a,n) /\ is_divisor(b,n)) thenis_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 -> Natis_divisor(a,b) isb ~= 0 /\a > b /\a - (a / b) * b = a,f : Nat ><Nat -> Natf(a,b) isif a=b then aelsif a-b > 0 then f(a-b,b) else f(a,b-a) endРешение:valuef : Nat ><Nat -> Natf(a,b) isif a=b then aelsif a-b > 0 then f(a-b,b) else f(a,b-a) end2. Доказать, что схема S2 является уточнением схемы S1:schemeS1 =classtype A,B,Cvaluef1 : A >< B -> Bool,f2 : A >< B -~-> C,f3 : C -~-> A >< Baxiomall a: A, b: B :f3( f2(a, b))is (a,b)pre f1(a,b) = trueend49schemeS2 =classtype A=Int, B=Nat, C=Intvaluef1 : A >< B -> Boolf1(i,n) is i * i = n,f2 : A >< B -~-> Cf2(i,n) is i,f3 : C -~-> A >< Bf3(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) = trueall_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:true3.

Дана алгебраическая спецификация группы функций, дать определениенеобходимых типов данных и явное определение функции get.schemeEXAM =classtype R, Key, Valvalueempty : Unit -> R,put : R >< Key >< Val -> R,del : R >< Key >< Val -~-> R,50get: R >< Key -~-> Val-set,find: R >< Key -> Bool,axiomforall 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) isif find (r, k1) thenget (r, k1) union {v1}else{v1}end,[del_put_1]del(put(r, k1, v1), k1, v1) isif find (r, k1) /\ v1 isin get (r, k1) thendel(r, k1, v1)elserend,[put_put]put(put(r, k1, v1), k2, v2) isif (k1 = k2) /\ (v1 = v2) thenput(r, k1, v1)elseput(put(r, k2, v2), k1, v1)endendРешение:type R = Key-m->Val-set, Key, Valvalueget: R >< Key -~-> Val-setget(r,k) as vspostvs = r(k)pre k isin dom r4.

Упростить выражение(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)515. Определить классы эквивалентности в пространстве входных значенийфункции f, отвечающие разбиению пространства в соответствии с критериемполноты тестового покрытия “все достижимые дизъюнкты” (AFDNF)postif (a > 5) /\ (b < 3) then ...elsif ((a > b) /\ (b=0)) \/ (b<3) then ...else ...endРешение:Ветвь 1: m1 m2Ветвь 2: нетВетвь 3: m1~m2 m3~m4~m2m1 ~m2 ~m3~m2~m1 m3 ~m4~m1~m3 m2~m1 m3 ~m4 m2~m1 m3 ~m4 ~m2~m1 ~m3 ~m2Ветвиm1 =a>5m2 =b<3m3 =a>bm4 =b=0m2 =b<3abДостижимыедизъюнкты1truetrue62m1 m22truefalsetruetrue2truefalsefalse-true2truefalsetruefalsetrue3truefalsetruefalsefalse64-false66m1~m2m3~m4~m2m1 ~m2 ~m3~m23truefalsefalse3false-truefalsetrue51~m1 m3 ~m43false-false-true12~m1~m3 m23false-truefalsetrue52~m1 m3 ~m4 m23false-truefalsefalse533false-false-false33~m1 m3 ~m4~m2~m1 ~m3 ~m2Пояснение.

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

valuef : Int >< Int-list >< Nat -~-> Nat >< Boolf (a,b,c) as (q,p)postif(a + len b > c) /\ (a isin elems b) then ...elsif(a>=c) /\ (a isin inds b)then ...else …endpre(a < c) \/ (a isin inds b)m2Ветвьm1m3m4a(a < c) (a isin (a + len b (a isininds b)> c)elems b)1truetruefalse1falsetruetruetrue2falsetruefalse2falsetruetruefalse3truefalse3truetruefalse2. postif (a > 4) /\ (b < 4) then ...elsif (a > b) /\ (b=4) then ...else ...endpre b<= 4Решение:postif m2 /\ m3 then ...elsif m4 /\ m5 then ...else ...endpre m153bсm1m3m4~m1m2m3m4~m1m2~m3~m1m2m3~m4m1~m3m1m3~m4B1 – m1m2m3B2 – m1m2~m3m4m5B3 – m1~m2~m4 \/m1~m2m4~m53.

postif (b > 5) /\ (a < 3) then ...elsif ((a > b) /\ (b=0)) \/ (b<5) then ...else ...endpre a+b<=7Решение:postif m2 /\ m3 then ...elsif (m4 /\ m5) \/ m6 then ...else ...endpre m1B1 – m1m2m3B2 – m1~m2m4m5m1~m2m4~m5m6m1~m2~m4m6B3 – m1~m2~m4~m64. postif (a isin dom b) /\ (b (a) = a) then ...elsif ((rng b inter dom b) = {}) \/ b(a+1) < 0 then ...else ...endpre(a isin dom b) /\ ((a+1) isin dom b)Решение:postif m1 /\ m3 then ...elsif m4 \/ m5 then ...else ...endprem1 /\ m2B1 – m1m2m3B2 – m1m2~m3~m4m5m1m2~m3m4B3 – m1m2~m3~m4~m5545.

postif (a > 5) /\ (b < 3) then ...elsif (a > b) \/ (b<3) then ...else ...endpre (a>2*b)Решение:postif m2 /\ m3 then ...elsif m4 \/ m3 then ...else ...endpre m1B1 – m1m2m3B2 – m1m2~m3m4 \/m1~m2m4 \/m1~m2~m4m3Тема: упрощение параллельных и недетерминированных выражений.1. (b!2) || (x:=a?) || if (a!3; true) |^| ((a!b?+5); false) then a!(b?)else a!(1+b?) end || (a!0)Решение:x:=3 || a!2 || a!0 |^|x:=0 || a!3 ; a!2 |^|x:=7 ; a!(1+b?) || a!0x:=0 || a!7; a!(1+b?)2. (if (a?)>0 then b!1 else b!2 end ++( a!1;x:=b?;b!4)) ||(y:= if (b?)=1 then a? else (0-a?) end) || (a!0)Решение:x:=1; y:=03.

(b!2) || (x:=a? |^| y:=b?) || (y:=a?) || if (true |^| false) then a!(b?)else a!(1+b?) endРешение:x:=2 || (y:=a?)|^|x:=3 || (y:=a?)|^|y:=2 || x:=a?|^|y:=3 || x:=a?|^|y:=2 || y:=b?|^|y:=3 || y:=b?|^|y:=2 || y:=a? || a!b?|^|y:=2 || y:=a? || a!(1+b?)554. (b!2) || (a!4; x:=a?) || (y:=a?) || if (true |^| false) then a!(b?)else a!(1+b?) endРешение:x:=2 || (y:=4)|^|x:=3 || (y:=4)|^|y:=2 || a!4; x:=a? |^|y:=3 || a!4; x:=a?5. a!(5+b?) || ((x:=(if true |^| false then x:=b?;1 else b!3;x:=2;6 end)+x) ++ (b!4 ||y:=b?))Решение:a!(5+b?) || x:=5; y:=b? |^|y:=3; x:=8; a!9|^|a!8 || x:=8 || y:=46.

case (1 |^| b?) of1 -> x:=a?+1,2 -> x:=b?,3 -> y:=a?+3,4 -> y:=b?+a?,5 -> x:=y:=a?;yend ||a!1 || b!(a?+2) || a!37. case (1 |^| b?) of1 -> x:=a?+1,2 -> x:=b? |^| a?,3 -> y:=a?+3,4 -> y:=b?+a?,5 -> x:=y:=a?;yend || a!0 || b!(a?+a?) || a!2 || a!38. (b!4 || y:=b?) || (a!(5+b?) ++ (x:=( x:=b!2; a? |^| b!3;x:=2;6)+x) )Решение:y:=4 || x:=14|^|y:=4 || x:=8 || a!8ЛИТЕРАТУРА1. The RAISE specification language. Prentice Hall, 1992.2.

RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994.3. B. Beizer. Software Testing Techniques, 2/e . New-York: Van Nostrand Reinhold,1990.4. B. Marick. The Craft of software Testing, PTR Prentice Hall, 1995.56СОДЕРЖАНИЕВведение ........................................................................................................................ 3Глава 1. Основные понятия языка RSL ....................................................................

51.1. Основные типы языка RSL. RSL логика ........................................................ 51.1.1. Встроенные типы языка RSL .................................................................... 51.1.2. Логика в языке RSL.................................................................................... 6Упражнения............................................................................................................. 71.2. Описание функций ........................................................................................... 91.2.1.

Декартовы произведения ( products ) ....................................................... 91.2.2. Описание констант ..................................................................................... 91.2.3. Описание функций ................................................................................... 101.2.3.1. Всюду вычислимые и частично вычислимые функции .................

101.2.3.2. Явный стиль описания функций....................................................... 111.2.3.3. Неявный стиль описания функций................................................... 111.2.3.4. Аксиоматическое описание функций...............................................

121.2.3.5. Схема определения функции ............................................................ 12Упражнения........................................................................................................... 131.3. Множества.......................................................................................................