МФСП, 03 семинар (от 15 сентября)
Материал из eSyr's wiki.
м |
|||
| Строка 158: | Строка 158: | ||
{{МФСП}} | {{МФСП}} | ||
| - | {{Lection-stub}} | ||
Версия 09:51, 29 сентября 2010
В прошлый раз рассматривались типы, операции с ними, производные типы. Разобрались с функциями, константами.
Сейчас: дорешать задачи пр функции и перейти к множествам.
Задача. Даны типы:
type position = Real×Real;
value
origin : Position = (0.0, 0.0) /* начало координат */
dist : Position × Position → Real
dist((x_1, y_1), (x_2, y_2)) ≡ ((x_1 - x_2)^2.0 + (y_1 - y_2)^2.0)^0.5
определить: тип circle, функцию on_circle
Решение:
type
Circle = Real × Position # радиус, центр
value
on_circle : Circle × Position → Bool
on_circle((r, c_0), c) ≡ (dist(c_0, c) = r)
Задача. Описать окружность с радиусом 3 и центром в начале координат.
value c_3_0_0 : Circle ≡ (3.0, Origin)
Задача. Описать точку, лежащую на этой окружности
Решение:
value d_on_c_3_0_0 : Position • on_circle(c_3_0_0, d_on_c_3_0_0) = True
Задача. Написать функцию sqrt, возвращающую значения, отличные от корня из x не более, чем на ε.
Решение:
value
sqrt : Real × Real; ⥲ Real
sqrt(a,b) as x
post (abs(sqrt(a) - x) ≤ b) && (x ≥ 0)
pre (b ≥ 0) && (a ≥ 0)
Задача. Дано определение:
value f: Int ⥲ Int f(x) ≡ f(x)
Удовлетворяет ли этому определению следующее определение:
value f: Int → Int f ≡ 1, chaos, 5 — все три раза да
Множества в RSL
Множество — конечный или бесконечный набор неповторяющихся элементов данного типа.
Обозначение:
{1, 2, 3}
В языке RSL множество определяется следующим образом:
- T - infset — для бесконечных множеств
- T - set — для конечных множеств
Для любого типа определено пустое множество — {}.
Над множеством определены следующие операции: ∩, ∪, ⊂, ⊃, ⊆, ⊇, ∉, ∈, \.
Другие операции:
card — размер множества:
card: T - infset ⥲ Nat card M ≡ |M|
card {} = 0
card {n|n:Nat} ≡ chaos
card {1,2,3} ≡ 3
Примеры:
- {"abc", "db", "efo"}
- {1..4} = {1,2,3,4}
- {4..1} = {}
Такое определение множества малоприменимо на практике, поэтому обычно множества определяют через выражения и ограничения:
{expr|limit}
Пример:
{2*n | n:Nat • n < 3} = {0, 2, 4}
Задача: даны типы Student, Course, и призводные типы:
type Student, Course, CourseIno = Course × Student-set University = Student-set × CourseInfo-set
Требуется:
- Определить для университета множество всех студентов (функция AllStudents)
- HasCourse — курс читается в университете
- NumberOk — каждый курс посещают не менее 5 и не более 100 человек
Решение:
value
AllStudents : University → Student-set
AllStudents ((s,ci)) ≡ s
HasCourse : Course × University → Bool
HasCourse(c,(s,ci)) ≡ ∃ (c, si) : CourseInfo • (c,si) ∈ ci
NumberOk : University → Bool
NumberOk((s, ci)) ≡ ∀ (c, s) : CourseInfo • (((c,s) ∈ ci) ⇒ ((card s > 5) ∧ (card s < 100)))
Почему импликация, а не конъюнкция:
value
c2 : Course
u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})}
При проверки с c=c2 получим false и значение функции false.
Задача. Описать функцию StudentOf, возвращающую множество студентов, посещающих заданный курс.
Решение:
value
StudentOf : Course × University → Student - set
StudentOf(c, (s, ci)) ≡ {st | st : Student • (c_i, st) : CourseInfo • ((c_i, st) ∈ ci) }
pre HasCourse(c, (s, ci)) ≡ True
Неявная спецификация:
value
StudentOf : Course × University → Student - set
pre HasCourse(c, (s, ci)) ≡ True
StudentOf(c, (s, ci)) as r
post
/* (r, c) ∈ c_i — для случая, если курсы уникальны */
∀ (c1, ss1) : CourseIno • (c1, ss1) ∈ ci ∧ r &ssub; ss1 ∧ ...
Задача. Функция, кторая возвращает множество курсов, которые посещает заданный студент.
Решение:
value
Attending : Student × University → Course - set
Attending(s, (st, ci)) ≡ {c | c : Course • (c, st_i) : CourseInfo • ((c, st_i) ∈ ci) ∧ (st ∈ st_i) }
Задача. Функция newStudent, добавляющая нового студента и возвращающая обновлённый университет. DropStud — удаляет студента.
Решение:
value
NewStud : University × Student ⥲ University
NewStud((ss, ci), s) ≡ (ss ∪ {s}, ci)
pre s ∉ ss
DropStud : University × Student ⥲ University
DropStud((ss, ci), s) ≡ (ss \ {s}, ci_1)
{(ss1, c) : CourseInfo • (ss1 ∪ s, c) ∈ cis ∧ s ∉ ss1}
pre s ∈ ss
post s ≠ ss ∧ &orall; (c, ss1) : CourseInfo • (c, ss1) ∈ cis → s ∈ cis
Задача. Удаление курса.
Решение:
DelCourse : University × Course → University
Формальная спецификация и верификация программ
|
|
