методичка (811291), страница 14
Текст из файла (страница 14)
5.1. (b) [(n, k) +> n \ k | n, k : Nat :- (n <= 50) /\ (k > 1) /\ (k < n)]
-
[n +> {k | k : Nat :- n \ k = 0 /\ k <= n /\ k >= 1} | n : Nat :- n <= 20]
-
[n +> m | n, m : Nat :- exists k : Nat :-
k * k = m /\ m <= n /\ (k + 1) * (k + 1) > n]
5.2. scheme
MAP_UNIVERSITY_SYSTEM =
class
type
Student,
Course,
CourseInfos = Course ‑m‑> Student-set,
University = Student-set >< CourseInfos
value
/* hasStudent проверяет, учится ли данный студент в указанном университете */
hasStudent : Student >< University -> Bool
hasStudent(s, (ss, cis)) is s isin ss,
hasCourse проверяет, читается ли данный курс в указанном университете */
hasCourse : Course >< University -> Bool
hasCourse(c, (ss, cis)) is c isin dom cis,
studOf возвращает множество студентов заданного университета, посещающих указанный курс
studOf : Course >< University -~-> Student-set
studOf(c, (ss, cis)) is cis(c)
pre hasCourse(c, (ss, cis)),
attending возвращает множество курсов, которые посещает данный студент в указанном университете
attending : Student >< University -~-> Course-set
attending(s, (ss, cis)) is
{c c : Course :- c isin dom cis /\ s isin cis(c)}
pre hasStudent(s, (ss, cis)),
newStud добавляет нового студента к числу студентов заданного университета
newStud : Student >< University -~-> University
newStud(s, (ss, cis)) is (ss union {s}, cis)
pre ~hasStudent(s, (ss, cis)),
dropStud исключает указанного студента из числа студентов заданного университета
dropStud : Student >< University -~-> University
dropStud(s, (ss, cis)) is
(ss \ {s}, [ c +> cis(c) \ {s} c : Course :- c isin dom cis ])
pre hasStudent(s, (ss, cis)),
newCourse добавляет новый курс с пустым множеством студентов к числу курсов заданного университета
newCourse : Course >< University -~-> University
newCourse(c, (ss, cis)) is (ss, cis !! [c +> {}])
pre ~hasCourse(c, (ss, cis)),
delCourse удаляет указанный курс из числа курсов заданного университета
delCourse : Course >< University -~-> University
delCourse(c, (ss, cis)) is (ss, cis \ {c})
pre hasCourse(c, (ss, cis))
end
6.1. scheme
STACK_ALG =
class
type Elem, Stack
value
empty : Stack,
push : Elem >< Stack -> Stack,
pop : Stack -~- Stack,
is_empty : Stack -> Bool,
top : Stack -~-> Elem
axiom
[ is_empty_empty ]
is_empty(empty) is true,
[ is_empty_push ]
all e : Elem, s : Stack :-
is_empty(push(e,s)) is false,
[ top_push ]
all e : Elem, s : Stack :-
top(push(e,s)) is e,
[ pop_push ]
all e : Elem, s : Stack :-
pop(push(e,s)) is s
end
6.3. scheme
STACK_LIST =
class
type Elem, Stack = Elem-list
value
empty : Stack = <..>,
push : Elem >< Stack -> Stack
push(e,s) is <. e .> ^ s,
pop : Stack -~- Stack
pop(s) is tl s
pre s ~= empty,
is_empty : Stack -> Bool
is_empty(s) is s = empty,
top : Stack -~-> Elem
top(s) is hd s
pre s ~= empty
end
Данная схема является уточнением схемы STACK_ALG, т.к. в ней определены все типы и функции из схемы STACK_ALG и справедливы все аксиомы исходной схемы. В качестве примера приведем доказательство справедливости аксиомы [top_push] для схемы STACK_LIST (справедливость остальных аксиом доказывается аналогично).
[ top_push ]
all e : Elem, s : Stack :-
top(push(e,s)) is e
[[раскрыть квантор]]
top(push(e,s)) is e
[[раскрыть идентификатор push]]
top(<. e .> ^ s) is e
[[раскрыть идентификатор top]]
hd (<. e .> ^ s) is e
[[вычислить hd]]
e is e
[[тождественное преобразование is]]
true
-
Да, вторая спецификация является уточнением первой. В качестве примера приведем доказательство справедливости третьей аксиомы (справедливость остальных аксиом доказывается аналогично).
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
7.1. type Record = = new_record(key_of : Key, data_of: Data)
Эквивалентное определение:
type Record
value
new_record : Key >< Data -> Record,
key_of : Record -> Key,
data_of : Record -> Data
axiom
all p : Record -> Bool :-
(all (k,d) : Key >< Data :-p(new_record(k,d))) => (all r : Record :- p(r)),
all k : Key, d : Data :- key_of(new_record(k,d)) = k,
all k : Key, d : Data :- data_of(new_record(k,d)) = d
7.2. type Stack = = empty | push(top : Elem, pop : Stack)
7.3. (b) type Tree
value
empty : Tree,
node : Tree >< Elem >< Tree -> Tree,
left : Tree -~-> Tree,
val : Tree -~-> Elem,
rigth : Tree -~-> Tree
axiom
[disjoint]
all t1,t2 :Tree, e : Elem:- empty ~= node(t1,e,t2),
[induction]
all p : Tree -> Bool :-
(p(empty) /\
(all t1,t2 : Tree, e : Elem:- p(t1) /\ p(t2) => p(node(t1,e,t2)))) =>
(all t : Tree :- p(t)),
[left_node]
all t1,t2 : Tree, e : Elem:- left(node(t1,e,t2)) is t1,
[val_node]
all t1,t2 : Tree, e : Elem:- val(node(t1,e,t2)) is e,
[right_node]
all t1,t2 : Tree, e : Elem:- right(node(t1,e,t2)) is t2
-
(a) x := 2
-
x := 2; 3
-
x := 1; 3
-
(a) scheme I_STACK_EX =
class
type Elem
variable st : Elem-list
value
empty : Unit -> write st Unit
empty() is st := <..>,
push : Elem -> write st Unit
push(e) is st := <. e .> ^ st,
pop : Unit -~-> write st Unit
pop() is st := tl st
pre st ~= <..>,
is_empty : Unit -> read st Bool
is_empty() is st = <..>,
top : Unit -~-> read st Elem
top() is hd st
pre st ~= <..>
end
8.2. (b) scheme I_STACK_IM =
class
type Elem
variable st : Elem-list
value
empty : Unit -> write st Unit
empty() post st = <..>,
push : Elem -> write st Unit
push(e) post st = <. e .> ^ st’,
pop : Unit -~-> write st Unit
pop() post st = tl st’
pre st ~= <..>,
is_empty : Unit -> read st Bool
is_empty() as b post b = (st = <..>),
top : Unit -~-> read st Elem
top() as e post e = hd st
pre st ~= <..>
end
8.3. (a) variable result : Real
value
fract_sum : Nat -~-> write result Unit
fract_sum(n) is
local variable counter : Nat := n in
result := 0.0;
while counter> 0 do
result := result + 1.0 / (real counter);
counter := counter – 1
end
end
pre n > 0
8.4. (a) 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 > с then d = с else x = y /\ d = a + b end) /\
(if с > 0 then x =c /\ d = b * с else x = x’ /\ d = b * (0 – с) end)
else (x = x’ /\ y =a + b /\ d = a + b /\ e = a - b) end
9.1. x := 1; (y := 1) ; (a!2) |^|
x := 1; (y := 1) ; (a!3)
9.2. x := 3 || a!2 || a!0 |^|
x := 0 || a!3 ; a!2 |^|
x := 7 ; a!(1 + b?) || a!0 |^|
x := 0 || a!7; a!(1 + b?)
-
x := 1; y := 0
-
x := 2 || b!5 |^|
x := 4 || b!3 |^|
y := 1; x := 1 |^|
y := 6
ЛИТЕРАТУРА
-
The RAISE specification language. Prentice Hall, 1992.
-
RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994.
-
Е.А. Кузьменкова, А.К. Петренко. Формальная спецификация программ на языке RSL (методическое пособие по практикуму), М., Изд-во АО "Диалог-МГУ", 1999.
-
Е.А. Кузьменкова, А.К. Петренко. Формальная спецификация программ на языке RSL (конспект лекций), М., Издательский отдел факультета ВМиК МГУ, 2001.
-
ftp://ftp.iist.unu.edu/pub/RAISE/course_material
СОДЕРЖАНИЕ
ВВЕДЕНИЕ 3
ГЛАВА 1. ОСНОВНЫЕ ТИПЫ ЯЗЫКА RSL. СПЕЦИФИКА RSL-ЛОГИКИ 5
Концепция типов в языке RSL 5
Описание подтипов 5
Встроенные типы языка RSL 5
Логика в языке RSL 6
Квантифицированные и условные выражения RSL 8
Упражнения 9
ГЛАВА 2. ОПИСАНИЕ КОНСТАНТ И ФУНКЦИЙ 11
Общая структура RSL спецификации 11
Декартовы произведения (products) 11
Выражение let 12
Описание констант 12
Всюду вычислимые и частично вычислимые функции 13
Явное описание функций 14
Неявное описание функций 15
Аксиоматическое описание функций 15
Схема определения функции 16
Упражнения 16
ГЛАВА 3. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. МНОЖЕСТВА 20
Понятие множества 20
Способы определения множеств 20
Операции над множествами 21
Упражнения 21
ГЛАВА 4. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ-ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. СПИСКИ 24
Понятие списка 24
Способы определения списков 24
Операции над списками 26
Выражение case 27
Упражнения 28
ГЛАВА 5. ОСНОВНЫЕ АБСТРАКЦИИ ДАННЫХ В МОДЕЛЕ‑ОРИЕНТИРОВАННЫХ СПЕЦИФИКАЦИЯХ. ОТОБРАЖЕНИЯ 30
Понятие отображения 30
Способы определения отображений 31
Операции над отображениями 32
Упражнения 33
ГЛАВА 6. АЛГЕБРАИЧЕСКИЕ СПЕЦИФИКАЦИИ 35
Понятие алгебраической спецификации 35
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
