Редактирование: МФСП, 03 семинар (от 15 сентября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
- | + | Продолжаем изучть язык RSL | |
- | + | В прошлый раз рассм. типы, операции с ними, призв. типы. Разбрались с функц., кнстантами. | |
+ | Сейчас: дорешать задачи пр функции и перейти к множествам. | ||
+ | |||
+ | Даны типы: | ||
- | '''Задача.''' Даны типы: | ||
'''type''' position = Real×Real; | '''type''' position = Real×Real; | ||
'''value''' | '''value''' | ||
- | origin : Position = (0.0, 0.0) | + | origin : Position = (0.0, 0.0) # начло координат |
dist : Position × Position → Real | 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 | dist((x_1, y_1), (x_2, y_2)) ≡ ((x_1 - x_2)^2.0 + (y_1 - y_2)^2.0)^0.5 | ||
Строка 13: | Строка 15: | ||
определить: тип circle, функцию on_circle | определить: тип circle, функцию on_circle | ||
- | '''Решение:''' | ||
'''type''' | '''type''' | ||
Circle = Real × Position # радиус, центр | Circle = Real × Position # радиус, центр | ||
Строка 20: | Строка 21: | ||
on_circle((r, c_0), c) ≡ (dist(c_0, c) = r) | on_circle((r, c_0), c) ≡ (dist(c_0, c) = r) | ||
- | + | Описать окр. с радиусм 3 и центром в нач. коорд. | |
'''value''' | '''value''' | ||
c_3_0_0 : Circle ≡ (3.0, Origin) | c_3_0_0 : Circle ≡ (3.0, Origin) | ||
- | + | Описать точку, лежащюю на этой окружности | |
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
d_on_c_3_0_0 : Position • on_circle(c_3_0_0, d_on_c_3_0_0) = True | d_on_c_3_0_0 : Position • on_circle(c_3_0_0, d_on_c_3_0_0) = True | ||
- | + | Написать sqrt, взвр. знач, отл. от корня из x не более, чем н eps. | |
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
- | sqrt : Real × Real; | + | sqrt : Real × Real; стрелочко с тильдой Real |
sqrt(a,b) as x | sqrt(a,b) as x | ||
- | '''post''' (abs(sqrt(a) - x) ≤ b) && (x ≥ 0) | + | '''post''' (abs(sqrt(a)-x) ≤ b) && (x ≥ 0) |
- | '''pre''' (b | + | '''pre''' (b ?ge; 0) && (a ≥ 0) |
- | + | Дано опр.: | |
'''value''' | '''value''' | ||
- | f: Int | + | f: Int стрелочка с тильдой Int |
f(x) ≡ f(x) | f(x) ≡ f(x) | ||
- | + | Удвл. ли этому опр. след. опр.: | |
'''value''' | '''value''' | ||
Строка 54: | Строка 53: | ||
== Множества в RSL == | == Множества в RSL == | ||
- | + | Конеч. или беск. набор. неповт. эл-тв дного типа. | |
- | + | Обозн: | |
{1, 2, 3} | {1, 2, 3} | ||
- | + | Опр. след. образом: | |
- | + | T - infset #для беск. | |
- | + | T - set #для конечных | |
- | Для | + | Для любго ипа опр. пустое мн-в — {} |
- | + | Опр. операции: ∩, &cuop, &sub, &ssub, &sube, &ssube, ∉, ∈, \ | |
- | + | card — рзмер множества: | |
- | + | card: T - infset стрелка с тильдоц Nat | |
- | + | ||
- | card: T - infset | + | |
card M ≡ |M| | card M ≡ |M| | ||
Строка 77: | Строка 74: | ||
card {1,2,3} ≡ 3 | card {1,2,3} ≡ 3 | ||
- | + | Примеры: | |
* {"abc", "db", "efo"} | * {"abc", "db", "efo"} | ||
* {1..4} = {1,2,3,4} | * {1..4} = {1,2,3,4} | ||
* {4..1} = {} | * {4..1} = {} | ||
- | Такое | + | Такое опр. мн-ва малоприменимо на практике, пэтому бычно мн-ва опр. через выр. и огр.: |
{expr|limit} | {expr|limit} | ||
- | + | Пример: | |
- | {2*n | n:Nat • n < 3} = {0, 2, 4} | + | {2*n|n:Nat • n < 3} = {0, 2, 4} |
- | + | Задача: даны типы Student, Course, и призв. типы: | |
'''type''' Student, Course, | '''type''' Student, Course, | ||
- | CourseIno = Course × Student-set | + | CourseIno = Course × Student -set |
- | University = Student-set × CourseInfo-set | + | University = Student - set × CourseInfo - set |
- | + | Задача: | |
- | * | + | * опр. для университета мн-во всех студентов (функция AllStudents) |
- | * | + | * HasCourse — курс читается в университете |
- | * | + | * NumberOk — каждый курс посещают не менее 5 и не более 100 человек |
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
- | AllStudents : University → Student-set | + | AllStudents : University → Student - set |
AllStudents ((s,ci)) ≡ s | AllStudents ((s,ci)) ≡ s | ||
HasCourse : Course × University → Bool | HasCourse : Course × University → Bool | ||
Строка 108: | Строка 104: | ||
Почему импликация, а не конъюнкция: | Почему импликация, а не конъюнкция: | ||
+ | |||
'''value''' | '''value''' | ||
c2 : Course | c2 : Course | ||
u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})} | u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})} | ||
- | При проверки с c=c2 получим | + | При проверки с c=c2 получим false и значение функции false. |
- | + | Описать функцию studentof, взвр. множество студентов, посещ. зад. курс. | |
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
StudentOf : Course × University → Student - set | StudentOf : Course × University → Student - set | ||
Строка 122: | Строка 118: | ||
'''pre''' HasCourse(c, (s, ci)) ≡ True | '''pre''' HasCourse(c, (s, ci)) ≡ True | ||
- | Неявная | + | Неявная спец.: |
'''value''' | '''value''' | ||
StudentOf : Course × University → Student - set | StudentOf : Course × University → Student - set | ||
Строка 128: | Строка 124: | ||
StudentOf(c, (s, ci)) as r | StudentOf(c, (s, ci)) as r | ||
'''post''' | '''post''' | ||
- | + | #(r, c) ∈ c_i --- для случая, если курсы уникальный | |
- | & | + | &orall; (c1, ss1) : CourseIno • (c1, ss1) ∈ ci ∧ r &ssub; ss1 ∧ ... |
- | + | Функция, кторая возвр. мн-ф курсов, которые псещ. заданный студент. | |
- | + | ||
- | + | ||
'''value''' | '''value''' | ||
Attending : Student × University → Course - set | Attending : Student × University → Course - set | ||
Attending(s, (st, ci)) ≡ {c | c : Course • (c, st_i) : CourseInfo • ((c, st_i) ∈ ci) ∧ (st ∈ st_i) } | Attending(s, (st, ci)) ≡ {c | c : Course • (c, st_i) : CourseInfo • ((c, st_i) ∈ ci) ∧ (st ∈ st_i) } | ||
- | + | Функция newStudent, добвл. нвог студента и взвр. обновл. университет. | |
+ | |||
+ | DropStud — удаляет студента | ||
- | '''Решение:''' | ||
'''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} | ||
Строка 152: | Строка 147: | ||
'''post''' s ≠ ss ∧ &orall; (c, ss1) : CourseInfo • (c, ss1) ∈ cis → s ∈ cis | '''post''' s ≠ ss ∧ &orall; (c, ss1) : CourseInfo • (c, ss1) ∈ cis → s ∈ cis | ||
- | + | ===Удаление курса=== | |
- | + | <math>DelCourse : University \times Course \rightarrow University </math> | |
- | + | ||
- | + | ||
{{МФСП}} | {{МФСП}} | ||
+ | {{Lection-stub}} |