МФСП, 03 семинар (от 15 сентября)
Материал из eSyr's wiki.
(→Множества в RSL) |
|||
| Строка 137: | Строка 137: | ||
'''value''' | '''value''' | ||
| - | NewStud : University | + | <math>NewStud : University\times Student\overset{\sim}{\rightarrow}University</math> |
NewStud((ss, ci), s) ≡ (ss ∪ {s}, ci) | NewStud((ss, ci), s) ≡ (ss ∪ {s}, ci) | ||
'''pre''' s ∉ ss | '''pre''' s ∉ ss | ||
| - | DropStud : University × Student | + | DropStud : University × Student <math>\overset{\sim}{\rightarrow}</math> University |
DropStud((ss, ci), s) ≡ (ss \ {s}, ci_1) | DropStud((ss, ci), s) ≡ (ss \ {s}, ci_1) | ||
{(ss1, c) : CourseInfo • (ss1 ∪ s, c) ∈ cis ∧ s ∉ ss1} | {(ss1, c) : CourseInfo • (ss1 ∪ s, c) ∈ cis ∧ s ∉ ss1} | ||
Версия 05:55, 27 сентября 2010
Продолжаем изучть язык RSL
В прошлый раз рассм. типы, операции с ними, призв. типы. Разбрались с функц., кнстантами.
Сейчас: дорешать задачи пр функции и перейти к множествам.
Даны типы:
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 не более, чем н eps.
value
sqrt : Real × Real; стрелочко с тильдой Real
sqrt(a,b) as x
post (abs(sqrt(a)-x) ≤ b) && (x ≥ 0)
pre (b ?ge; 0) && (a ≥ 0)
Дано опр.:
value f: Int стрелочка с тильдой Int f(x) ≡ f(x)
Удвл. ли этому опр. след. опр.:
value f: Int → Int f ≡ 1, chaos, 5 — все три раза да
Множества в RSL
Конеч. или беск. набор. неповт. эл-тв дного типа.
Обозн:
{1, 2, 3}
Опр. след. образом:
T - infset #для беск. T - set #для конечных
Для любго ипа опр. пустое мн-в — {}
Опр. операции: ∩, &cuop, &sub, &ssub, &sube, &ssube, ∉, ∈, \
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 --- для случая, если курсы уникальный
&orall; (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 — удаляет студента
valueNewStud((ss, ci), s) ≡ (ss ∪ {s}, ci) pre s ∉ ss
DropStud : University × StudentUniversity 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
Формальная спецификация и верификация программ
|
|
