Е.А. Кузьменкова, А.К. Петренко - Формальная спецификация программ на языке RSL (1158800), страница 9
Текст из файла (страница 9)
B2 – m1m2~m3m4m5
B3 – m1~m2~m4 \/
m1~m2m4~m5
3. post
if (b > 5) /\ (a < 3) then ...
elsif ((a > b) /\ (b=0)) \/ (b<5) then ...
else ...
end
pre a+b<=7
Решение:
post
if m2 /\ m3 then ...
elsif (m4 /\ m5) \/ m6 then ...
else ...
end
pre m1
B1 – m1m2m3
B2 – m1~m2m4m5
m1~m2m4~m5m6
m1~m2~m4m6
B3 – m1~m2~m4~m6
4. post
if (a isin dom b) /\ (b (a) = a) then ...
elsif ((rng b inter dom b) = {}) \/ b(a+1) < 0 then ...
else ...
end
pre
(a isin dom b) /\ ((a+1) isin dom b)
Решение:
post
if m1 /\ m3 then ...
elsif m4 \/ m5 then ...
else ...
end
pre
m1 /\ m2
B1 – m1m2m3
B2 – m1m2~m3~m4m5
m1m2~m3m4
B3 – m1m2~m3~m4~m5
5. post
if (a > 5) /\ (b < 3) then ...
elsif (a > b) \/ (b<3) then ...
else ...
end
pre (a>2*b)
Решение:
post
if m2 /\ m3 then ...
elsif m4 \/ m3 then ...
else ...
end
pre m1
B1 – m1m2m3
B2 – 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!0
x:=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:=0
3. (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?)
4. (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:=4
6. case (1 |^| b?) of
1 -> x:=a?+1,
2 -> x:=b?,
3 -> y:=a?+3,
4 -> y:=b?+a?,
5 -> x:=y:=a?;y
end ||
a!1 || b!(a?+2) || a!3
7. case (1 |^| b?) of
1 -> x:=a?+1,
2 -> x:=b? |^| a?,
3 -> y:=a?+3,
4 -> y:=b?+a?,
5 -> x:=y:=a?;y
end || a!0 || b!(a?+a?) || a!2 || a!3
8. (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.
СОДЕРЖАНИЕ
Введение 3
Глава 1. Основные понятия языка RSL 5
1.1. Основные типы языка RSL. RSL логика 5
1.1.1. Встроенные типы языка RSL 5
1.1.2. Логика в языке RSL 6
Упражнения 7
1.2. Описание функций 9
1.2.1. Декартовы произведения ( products ) 9
1.2.2. Описание констант 9
1.2.3. Описание функций 10
1.2.3.1. Всюду вычислимые и частично вычислимые функции 10
1.2.3.2. Явный стиль описания функций 11
1.2.3.3. Неявный стиль описания функций 11
1.2.3.4. Аксиоматическое описание функций 12
1.2.3.5. Схема определения функции 12
Упражнения 13
1.3. Множества 15
1.3.1. Понятие множества 15
1.3.2. Способы определения множеств 16
Упражнения 17
1.4. Списки 18
1.4.1. Понятие списка 18
1.4.2. Способы определения списков 18
1.4.3. Операции над списками 20
Упражнения 20
1.5. Отображения (maps) 21
1.5.1. Понятие отображения 21
1.5.2. Способы определения отображений 22
1.5.3. Операции над отображениями 23
Упражнения 25
Глава 2. Задание практикума 26
2.1. Постановка задачи 26
2.2. Варианты заданий 26
2.3. Методические рекомендации 30
Глава 3. Сценарий работы с редактором eden 31
3.1. Начало работы с редактором 31
3.2. Командное меню редактора 33
3.3. Редактирование модуля 34
3.4. Обработка ошибок редактирования 38
3.5. Завершение редактирования модуля 41
Ответы и решения к упражнениям главы 1 44
Пример варианта письменного экзамена
и его решение 49
ЛИТЕРАТУРА 56
58
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
