Редактирование: МФСП, 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)) | + | 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 | определить: тип circle, функцию on_circle | ||
- | '''Решение:''' | ||
'''type''' | '''type''' | ||
Circle = Real × Position # радиус, центр | Circle = Real × Position # радиус, центр | ||
'''value''' | '''value''' | ||
on_circle : Circle × Position → Bool | on_circle : Circle × Position → Bool | ||
- | on_circle((r, c_0), c) | + | on_circle((r, c_0), c) == (dist(c_0, c) = r) |
- | + | Описать окр. с радиусм 3 и центром в нач. коорд. | |
'''value''' | '''value''' | ||
- | c_3_0_0 : Circle | + | c_3_0_0 : Circle == (3.0, Origin) |
- | + | Описать точку, лежащюю на этой окружности | |
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
- | d_on_c_3_0_0 : Position & | + | 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) |
- | + | Удвл. ли этому опр. след. опр.: | |
'''value''' | '''value''' | ||
f: Int → Int | f: Int → Int | ||
- | f | + | f == 1, chaos, 5 — все три раза да |
- | + | Множества в RSL | |
- | + | Конеч. или беск. набор. неповт. эл-тв дного типа. | |
- | + | Обозн: | |
{1, 2, 3} | {1, 2, 3} | ||
- | + | Опр. след. образом: | |
- | + | T - infset #для беск. | |
- | + | T - set #для конечных | |
- | Для | + | Для любго ипа опр. пустое мн-в — {} |
- | + | Опр. операции: ∩, &cuop, &sub, &ssub, &sube, &ssube, ∉, ∈, \ | |
- | + | card — рзмер множества: | |
- | + | card: T - infset стрелка с тильдоц Nat | |
- | + | card M == |M| | |
- | card: T - infset | + | |
- | card M | + | |
card {} = 0 | card {} = 0 | ||
- | card {n|n:Nat} | + | card {n|n:Nat} == chaos |
- | card {1,2,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 & | + | {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)) | + | AllStudents ((s,ci)) == s |
HasCourse : Course × University → Bool | HasCourse : Course × University → Bool | ||
- | HasCourse(c,(s,ci)) | + | HasCourse(c,(s,ci)) == ∃ (c, si) : CourseInfo ˙ (c,si) ∈ ci |
NumberOk : University → Bool | NumberOk : University → Bool | ||
- | NumberOk((s, ci)) | + | NumberOk((s, ci)) == ∀ (c, s) : CourseInfo ˙ (((c,s) ∈ ci) ⇒ ((card s > 5) ∧ (card s < 100))) |
Почему импликация, а не конъюнкция: | Почему импликация, а не конъюнкция: | ||
+ | |||
'''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 | ||
- | StudentOf(c, (s, ci)) | + | StudentOf(c, (s, ci)) == {st | st : Student ˙ (c_i, st) : CourseInfo ˙ ((c_i, st) ∈ ci) } |
- | '''pre''' HasCourse(c, (s, ci)) | + | '''pre''' HasCourse(c, (s, ci)) == True |
- | Неявная | + | Неявная спец.: |
'''value''' | '''value''' | ||
StudentOf : Course × University → Student - set | StudentOf : Course × University → Student - set | ||
- | '''pre''' HasCourse(c, (s, ci)) | + | '''pre''' HasCourse(c, (s, ci)) == True |
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)) | + | Attending(s, (st, ci)) == {c | c : Course ˙ (c, st_i) : CourseInfo ˙ ((c, st_i) ∈ ci) ∧ (st ∈ st_i) } |
- | + | Функция newStudent, добвл. нвог студента и взвр. обновл. университет. | |
+ | |||
+ | DropStud — удаляет студента | ||
- | '''Решение:''' | ||
'''value''' | '''value''' | ||
- | NewStud : University × Student | + | NewStud : University × Student стрелочк с тильдой University |
- | NewStud((ss, ci), s) | + | NewStud((ss, ci), s) == (ss ∪ {s}, ci) |
'''pre''' s ∉ ss | '''pre''' s ∉ ss | ||
- | DropStud : University × Student | + | DropStud : University × Student стрелочк с тильдой University |
- | DropStud((ss, ci), s) | + | DropStud((ss, ci), s) == (ss \ {s}, ci_1) |
- | {(ss1, c) : CourseInfo & | + | {(ss1, c) : CourseInfo ˙ (ss1 ∪ s, c) ∈ cis ∧ s ∉ ss1} |
'''pre''' s ∈ ss | '''pre''' s ∈ ss | ||
- | '''post''' s ≠ ss ∧ &orall; (c, ss1) : CourseInfo & | + | '''post''' s ≠ ss ∧ &orall; (c, ss1) : CourseInfo ˙ (c, ss1) ∈ cis → s ∈ cis |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
{{МФСП}} | {{МФСП}} | ||
+ | {{Lection-stub}} |