Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL (Е.А. Кузьменкова, А.К. Петренко - практикум на языке RSL.pdf), страница 13

Описание сигнатур этих функцийостается фактически неизменным во всех трех видах спецификаций (явном,неявном, алгебраическом).При разработке моделе-ориентированных спецификаций необходимо выбратьподходящую абстракцию данных и на ее основе промоделировать заданнуюпрограммную систему. В качестве абстракции данных в зависимости от спецификирешаемой задачи можно использовать имеющиеся в языке RSL абстракциимножеств, списков и отображений. Набор операций должен содержать операции,позволяющие накапливать в системе необходимую информацию, т.е. осуществлятьнаполнение некоторой информационной базы системы, способ представлениякоторой определяется выбранной абстракцией данных.

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

если вуказанное время у этой группы и преподавателя нет других занятий и свободнауказанная аудитория. Одним из важных средств описания консистентногосостояния являются инварианты, которые в RSL представляются либо в формеаксиом, либо в форме ограничений подтипов.Весьма распространенным способом определения ограничения подтипаявляется использование для этой цели предиката-ограничения, представленного ввиде функции is_wf_system(sys), с помощью которой проверяется сохранениеинвариантов в моделируемой системе.

В качестве примера рассмотриммоделирование базы данных, хранящей совокупность записей вида «ключ данные», на основе абстракции множеств. Предикат is_wf_db(rs) задаетограничение подтипа, позволяющее из произвольных множеств записей указанноговида отбирать только те, которые удовлетворяют условию «хорошосформированной» базы данных, т.е. гарантируют сохранение свойствауникальности ключа для всех записей в базе данных.typeKey, Data, Record = Key >< Data,DataBase={| rs : Record-set :- is_wf_db(rs)|}valueis_wf_db : Record-set -> Boolis_wf_db(rs) is (all k : Key, d1,d2 : Data :((k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2)Кроме указанных основных операций по наполнению информационной базысистемы полезно предусмотреть операции, позволяющие изменять отдельныеэлементы базы, а также осуществлять в базе поиск полезной с точки зренияразработчика спецификаций информации.

Некоторые примеры таких операцийприводятся в описании вариантов заданий практикума, однако их набор можетбыть расширен по желанию разработчика спецификаций.При разработке неявных спецификаций функций следует обращать особоевнимание на строгость формулировки постусловия, стараясь как можно тщательнееописать там результат выполнения функции и избежать по возможностивозникновения неполной спецификации. Иллюстрацией неполной спецификацииподобного рода может служить следующая спецификация функции добавленияновой записи в описанную выше базу данных:valueadd : Key >< Data >< DataBase -~-> DataBaseadd(k,d,db) as respost (k,d) isin dbpre (k,d) ~ isin db68Предложенная спецификация является неполной, т.к. лишь частичноописывает эффект от добавления нового элемента (k,d) в множество db.

Вчастности, здесь игнорируется важный факт, что добавление элемента являетсяединственным изменением, производимым функцией add над множеством db, и,следовательно, за исключением элемента (k,d) множества db и res должныполностью совпадать.69ГЛАВА 12. ПРИМЕРЫ ЭКЗАМЕНАЦИОННЫХ БИЛЕТОВБилет № 1.1. Дано explicit определение функции. Написать implicit-спецификацию функцииэквивалентной данной.valuef : Int ><Int >< Int -> write x read y Int >< Intf(a,b,c) isif a=b then(if a+b > c then c else a+b end,a*b*(if c>0 then x:=y; c else 0-c end))else (a+b, x:=b; a-b)endРешение:valuef : Int ><Int >< Int -> write x read y Int >< Intf(a,b,c) as (d, e)postif a=b thenif a+b>c thenif c>0 then d=c /\ x=y /\ e = a*b*celse d=c /\ x=x’ /\ e=a*b*(0-c) endelseif c>0 then d=a+b /\ x=y /\ e= a*b*celse d=a+b /\ x=x‘ /\ e=a*b*(0-c) endelse d=a+b /\ x=b /\ e=a-bend2.

Дать явное (explicit) или неявное (implicit) определение функций (включаяслабейшие предусловия), отвечающих требованиям аксиом:type S, Evaluecreate : Unit -> S,add : E >< S -> S,del : S -~-> S,next : S -~-> S,get : S -~-> E,append : S >< S -> Saxiomall e : E, s : S :del( add( e, s ) ) is s,all e : E, s : S :get( add( e, s ) ) is e,all e : E, s : S :next( add( e, s )) isif s = create( ) then add( e, s )else append ( s, add( e, create( ) )end,all e : E, s1, s2 : S :append( create(), s2 )) is s2,all e : E, s1, s2 : S :append( add(e, s1), s2 )) isadd (e, append (s1, s2))Решение:type S, Evaluecreate : Unit -> Screate is <..>,70add : E >< S -> Sadd (e,s) is <.e.> ^ s,del : S -~-> Sdel (s) is tl spre s~=<..>,next : S -~-> Snext (s) is tl s ^ <.

hd s .>pre s~= <..>,get : S -~-> Eget (s) is hd spre s ~= <..>,append : S >< S -> Sappend (s1, s2) as spostif s1=<..> then s=s2else s=add(hd s1, append( tl s1, s2))end3. Доказать, что правая спецификация является (или не является) уточнениемлевой.valuef1 : M >< M -> M,f2 : M -> S >< S,f3 : E >< S -> Bool,f4 : E >< E -> Maxiomall a1, a2, b1, b2 : E :let (p,q) = f2(f1(f4 (a1,b1), f4(a2,b2)))inf3(a1,p) /\ f3(b1,q) /\ f3(a2,p) /\ f3(b2,q)end is truetypeM = E –m-> E,S = E-setvaluef1 : M >< M -> Mf1(m1,m2) is m1 !! m2,f2 : M -> S >< Sf2(m) is (dom m, rng m),f3 : E >< S -> Boolf3(a,b) is a isin b,f4 : E >< E -> Mf4(a,b) is [a +> b]Решение:[[раскрыть all]]let (p, q) = f2(f1(f4(a1, b1), f4(a2, b2))) inf3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) endis true[[раскрыть f4]]let (p, q) = f2(f1([a1 +>b1], [a2+>b2])) inf3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) endis true[[раскрыть f1]]let (p, q) = f2([a1 +>b1, a2+>b2]) inf3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) endis true71[[раскрыть f2]]let (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end inf3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) endis true[[раскрыть f3]]let (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end ina1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q endis true[[вычислить]]let (p, q) = ({a1, a2}, if a1=a2 then {b2} else {b1, b2} end ina1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q endis true[[раскрыть let]]a1 isin {a1, a2} /\ b1 isin if a1=a2 then {b2} else {b1, b2} end /\ a2 isin {a1, a2} /\ b2 isin ifa1=a2 then {b2} else {b1, b2} end endis true[[вычислить]]true /\ b1 isin if a1=a2 then {b2} else {b1, b2} end /\ true /\ b2 isin if a1=a2 then {b2} else {b1,b2} end endis true[[упростить /\ ]]b1 isin if a1=a2 then {b2} else {b1, b2} end /\ b2 isin if a1=a2 then {b2} else {b1, b2} end endis true[[вычислить if]]b1 isin if a1=a2 then {b2} else {b1, b2} end /\ trueis true[[упростить /\ ]]b1 isin if a1=a2 then {b2} else {b1, b2} endis true[[анализ case]][[non_eq]] ~a1=a2 [[eq]] a1=a2[[ предположение non_eq ]] ~a1=a2b1 isin {b1, b2}is true[[вычислить ]]trueis truetrue[[ предположение eq ]] a1=a2b1 isin {b2}is true[[вычислить]]72falseis truefalseОтвет: Нет, правая спецификация не является уточнением левой.4.

Дано определение вариантного типа:type Elem, Collection == empty | add (Collection <-> head, first:Elem, Elem <-> new_second)Дать эквивалентное определение без использования вариантных определений.Решение:type Elem, Collectionvalue empty : Collection,add : Collection >< Elem >< Elem -> Collection,head : Collection >< Collection -~-> Collection,first : Collection -~-> Elem,new_second : Elem >< Collection -~-> Collectionaxiom[disjoint]all c,c1 ; Collection, e1, e2 ; Elem :empty ~= add(c, e1, e2)[induction]all isCollection ; Collection -> Bool :isCollection(empty) /\ (all c1 : Collection, e1, e2 ; Elem :- (isCollection(c1) =>isCollection(add(c1, e1, e2)))) =>(all c2 : Collection :- isCollection ( c2 ))[head_add]all c1, c2 ; Collection, e1, e2 : Elem :- head (c1, add(c2, e1, e2)) is add(c1, e1, e2))[first_add]all c: Collection, e1, e2 : Elem :- first (add(c, e1, e2)) is e1[new_second_add]all c: Collection, e1, e2, e3 : Elem :- new_second (e1, add(e2, e3)) is add(c, e2,e1)73Билет № 2.1.

Дано explicit определение функции. Написать implicit-спецификацию функцииэквивалентной данной.valuef : Int >< Int -> write x read y Int >< Int >< Intf (a, b) islocal variable v : Int := 0 inx:=0;for i in <.a..b.> dox:=x+y; v := v+2*iend; (a,b,v+y)endРешение:valuef : Int >< Int -> write x read y Int >< Int >< Intf (a, b) as (c, d, e)posta = c /\ b = d /\if a > b then e = y /\ x = 0else x = y * (b-a+1) /\ e = (a+b)*(b-a+1)+yend2.

Дать explicit или implicit определение функций (включая слабейшиепредусловия), отвечающее требованиям аксиом:type S, Evaluecreate : Unit -> S,push_down : E >< S -> S,push_right : E >< S -> S,pop_up : S -~-> S,pop_left : S -~-> S,get : S -~-> E,axiomall e : E, s : S :pop_up( push_down( e, s ) ) is s,all e : E, s : S :pop_up( push_right( e, s ) ) is pop_up( s ),all e : E, s : S :get( push_down( e, s ) ) is e,all e : E, s : S :get( push_right( e, s ) ) is e,all e : E, s : S :pop_left( push_right( e, s ) ) is sРешение:type S = L-list, L = E-list, Evaluecreate : Unit -> Screate () is <..>,push_down : E >< S -> Spush_down (e,s) is <.

<. E .> .> ^ S,push_right : E >< S -> Spush_right (e,s) isif s = <..> then <. <. e .> .>else <. <. e .> ^ hd s .> ^ tl send,pop_up S -~-> S74pop_up (s) is tl spre s ~= <..>,pop_left : S -~-> Spop_left (s) is <. tl hd s .> ^ tl spre s~= <..> /\ hd s~=<..>,get : S -~-> Eget (s) is hd hd spre s~ ~= <..> /\ hd s~ ~= <..>3.