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

• инициализацию информационной базы пустым значением (в RSL это выражается путем определения соответствующей константы),

• добавление в базу нового элемента,

• удаление указанного элемента из базы.

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

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

type

Key, Data, Record = Key >< Data,

DataBase={| rs : Record-set :- is_wf_db(rs)|}

value

is_wf_db : Record-set -> Bool

is_wf_db(rs) is (all k : Key, d1,d2 : Data :-

((k,d1) isin rs /\ (k,d2) isin rs) => d1 = d2)

Кроме указанных основных операций по наполнению информационной базы системы полезно предусмотреть операции, позволяющие изменять отдельные элементы базы, а также осуществлять в базе поиск полезной с точки зрения разработчика спецификаций информации. Некоторые примеры таких операций приводятся в описании вариантов заданий практикума, однако их набор может быть расширен по желанию разработчика спецификаций.

При разработке неявных спецификаций функций следует обращать особое внимание на строгость формулировки постусловия, стараясь как можно тщательнее описать там результат выполнения функции и избежать по возможности возникновения неполной спецификации. Иллюстрацией неполной спецификации подобного рода может служить следующая спецификация функции добавления новой записи в описанную выше базу данных:

value

add : Key >< Data >< DataBase -~-> DataBase

add(k,d,db) as res

post (k,d) isin db

pre (k,d) ~ isin db

Предложенная спецификация является неполной, т.к. лишь частично описывает эффект от добавления нового элемента (k,d) в множество db. В частности, здесь игнорируется важный факт, что добавление элемента является единственным изменением, производимым функцией add над множеством db, и, следовательно, за исключением элемента (k,d) множества db и res должны полностью совпадать.

Глава 12. ПРИМЕРЫ ЭКЗАМЕНАЦИОННЫХ БИЛЕТОВ

Билет № 1.

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 a+b end,

a*b*(if c>0 then x:=y; c else 0-c end))

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

end

Решение:

value

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

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

post

if a=b then

if a+b>c then

if c>0 then d=c /\ x=y /\ e = a*b*c

else d=c /\ x=x’ /\ e=a*b*(0-c) end

elseif c>0 then d=a+b /\ x=y /\ e= a*b*c

else d=a+b /\ x=x‘ /\ e=a*b*(0-c) end

else d=a+b /\ x=b /\ e=a-b

end

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

Решение:

type S, E

value

create : Unit -> S

create is <..>,

add : E >< S -> S

add (e,s) is <.e.> ^ s,

del : S -~-> S

del (s) is tl s

pre s~=<..>,

next : S -~-> S

next (s) is tl s ^ <. hd s .>

pre s~= <..>,

get : S -~-> E

get (s) is hd s

pre s ~= <..>,

append : S >< S -> S

append (s1, s2) as s

post

if s1=<..> then s=s2

else s=add(hd s1, append( tl s1, s2))

end

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

Решение:

[[раскрыть all]]

let (p, q) = f2(f1(f4(a1, b1), f4(a2, b2))) in

f3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end

is true

[[раскрыть f4]]

let (p, q) = f2(f1([a1 +>b1], [a2+>b2])) in

f3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end

is true

[[раскрыть f1]]

let (p, q) = f2([a1 +>b1, a2+>b2]) in

f3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end

is true

[[раскрыть f2]]

let (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end in

f3(a1, p) /\ f3(b1, q) /\ f3(a2, p) /\ f3(b2,q) end

is true

[[раскрыть f3]]

let (p, q) = if a1=a2 then ({a1, a2}, {b2}) else ({a1, a2}, {b1, b2}) end in

a1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q end

is true

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

let (p, q) = ({a1, a2}, if a1=a2 then {b2} else {b1, b2} end in

a1 isin p /\ b1isin q /\ a2 isin p /\ b2 isin q end

is true

[[раскрыть let]]

a1 isin {a1, a2} /\ b1 isin if a1=a2 then {b2} else {b1, b2} end /\ a2 isin {a1, a2} /\ b2 isin if a1=a2 then {b2} else {b1, b2} end end

is 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 end

is true

[[упростить /\ ]]

b1 isin if a1=a2 then {b2} else {b1, b2} end /\ b2 isin if a1=a2 then {b2} else {b1, b2} end end

is true

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

b1 isin if a1=a2 then {b2} else {b1, b2} end /\ true

is true

[[упростить /\ ]]

b1 isin if a1=a2 then {b2} else {b1, b2} end

is true

[[анализ case]]

[[non_eq]] ~a1=a2 [[eq]] a1=a2

[[ предположение non_eq ]] ~a1=a2

b1 isin {b1, b2}

is true

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

true

is true

true

[[ предположение eq ]] a1=a2

b1 isin {b2}

is true

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

false

is true

false

Ответ: Нет, правая спецификация не является уточнением левой.

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

type Elem, Collection == empty | add (Collection <-> head, first:Elem, Elem <-> new_second)

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

Решение:

type Elem, Collection

value empty : Collection,

add : Collection >< Elem >< Elem -> Collection,

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

first : Collection -~-> Elem,

new_second : Elem >< Collection -~-> Collection

axiom

[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)

Билет № 2.

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

value

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

f (a, b) is

local variable v : Int := 0 in

x:=0;

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

x:=x+y; v := v+2*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

a = c /\ b = d /\

if a > b then e = y /\ x = 0

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

end

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

Решение:

type S = L-list, L = E-list, E

value