методичка (Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL), страница 14
Описание файла
Документ из архива "Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL", который расположен в категории "". Всё это находится в предмете "формальная спецификация и верификация программ" из 9 семестр (1 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Онлайн просмотр документа "методичка"
Текст 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
