Редактирование: МФСП, 03 семинар (от 15 сентября)

Материал из eSyr's wiki.

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Продолжаем изучть язык RSL

В прошлый раз рассм. типы, операции с ними, призв. типы. Разбрались с функц., кнстантами.

Сейчас: дорешать задачи пр функции и перейти к множествам.

Даны типы:

'''type''' position = Real&times;Real;
 '''value'''
   origin : Position = (0.0, 0.0) # начло координат
   dist : Position &times; Position &rarr; 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 &times; Position # радиус, центр
 '''value'''
   on_circle : Circle &times; Position &rarr; 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 &dot; on_circle(c_3_0_0, d_on_c_3_0_0) = True

Написать sqrt, взвр. знач, отл. от корня из x не более, чем н eps.

'''value'''
   sqrt : Real &times; Real; стрелочко с тильдой Real
     sqrt(a,b) as x
     '''post''' (abs(sqrt(a)-x) &le; b) && (x &ge; 0)
     '''pre''' (b ?ge; 0) && (a &ge; 0)

Дано опр.:

'''value'''
   f: Int стрелочка с тильдой Int
   f(x) == f(x)

Удвл. ли этому опр. след. опр.:

'''value'''
   f: Int &rarr; Int
    f == 1, chaos, 5 — все три раза да

Множества в RSL

Конеч. или беск. набор. неповт. эл-тв дного типа.

Обозн: 
 {1, 2, 3}

Опр. след. образом:
 T - infset #для беск.
 T - set #для конечных

Для любго ипа опр. пустое мн-в — {}

Опр. операции: &cap;, &cuop, &sub, &ssub, &sube, &ssube, &notin;, &isin;, \

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 &dot; n &lt; 3} = {0, 2, 4}

Задача: даны типы Student, Course, и призв. типы: 
 '''type''' Student, Course, 
   CourseIno = Course &times; Student -set
   University =  Student - set &times; CourseInfo - set

Задача: 
* опр. для университета мн-во всех студентов (функция AllStudents)
* HasCourse — курс читается в университете
* NumberOk — каждый курс посещают не менее 5 и не более 100 человек

'''value'''
   AllStudents : University &rarr; Student - set
     AllStudents ((s,ci)) == s
   HasCourse : Course &times; University &rarr; Bool
     HasCourse(c,(s,ci)) == &exist; (c, si) : CourseInfo &dot; (c,si) &isin; ci
   NumberOk : University &rarr; Bool
     NumberOk((s, ci)) == &forall; (c, s) : CourseInfo &dot; (((c,s) &isin; ci) &rArr; ((card s &gt; 5) &and; (card s &lt; 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 &times; University  &rarr; Student - set
     StudentOf(c, (s, ci)) == {st | st : Student &dot; (c_i, st) : CourseInfo &dot; ((c_i, st) &isin; ci) }
     '''pre''' HasCourse(c, (s, ci)) == True

Неявная спец.:
 '''value'''
   StudentOf : Course &times; University  &rarr; Student - set
     '''pre''' HasCourse(c, (s, ci)) == True
     StudentOf(c, (s, ci)) as r
     '''post''' 
       #(r, c)  &isin; c_i --- для случая, если курсы уникальный
       &orall; (c1, ss1) : CourseIno &dot; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...

Функция, кторая возвр. мн-ф курсов, которые псещ. заданный студент.
 '''value'''
   Attending : Student &times; University  &rarr; Course - set
     Attending(s, (st, ci)) == {c | c : Course &dot; (c, st_i) : CourseInfo &dot; ((c, st_i) &isin; ci) &and; (st &isin; st_i) }

Функция newStudent, добвл. нвог студента и взвр. обновл. университет.

DropStud — удаляет студента

'''value''' 
   NewStud : University &times; Student стрелочк с тильдой University
     NewStud((ss, ci), s) == (ss &cup; {s}, ci)
     '''pre''' s &notin; ss

DropStud : University &times; Student стрелочк с тильдой University
     DropStud((ss, ci), s) == (ss \ {s}, ci_1) 
     {(ss1, c) : CourseInfo &dot; (ss1 &cup; s, c) &isin; cis &and; s &notin; ss1}
     '''pre''' s &isin; ss
     '''post''' s &ne; ss &and; &orall; (c, ss1) : CourseInfo &dot; (c, ss1) &isin; cis &rarr; s &isin; cis

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.us/wiki/%D0%9C%D0%A4%D0%A1%D0%9F%2C_03_%D1%81%D0%B5%D0%BC%D0%B8%D0%BD%D0%B0%D1%80_%28%D0%BE%D1%82_15_%D1%81%D0%B5%D0%BD%D1%82%D1%8F%D0%B1%D1%80%D1%8F%29

Редактирование: МФСП, 03 семинар (от 15 сентября)

Материал из eSyr's wiki.

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 1: / Строка 1: @@
-В прошлый раз рассматривались типы, операции с ними, производные типы. Разобрались с функциями, константами.
+Продолжаем изучть язык RSL
-Сейчас: дорешать задачи про функции и перейти к множествам.
+В прошлый раз рассм. типы, операции с ними, призв. типы. Разбрались с функц., кнстантами.
+Сейчас: дорешать задачи пр функции и перейти к множествам.
+Даны типы:
-'''Задача.''' Даны типы:
  '''type''' position = Real&times;Real;
  '''value'''
-   origin : Position = (0.0, 0.0) /* начало координат */
+   origin : Position = (0.0, 0.0) # начло координат
    dist : Position &times; Position &rarr; Real
-     dist((x_1, y_1), (x_2, y_2)) &equiv; ((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
 определить: тип circle, функцию on_circle
-'''Решение:'''
  '''type'''
    Circle = Real &times; Position # радиус, центр
  '''value'''
    on_circle : Circle &times; Position &rarr; Bool
-     on_circle((r, c_0), c) &equiv; (dist(c_0, c) = r)
+     on_circle((r, c_0), c) == (dist(c_0, c) = r)
-'''Задача.''' Описать окружность с радиусом 3 и центром в начале координат.
+Описать окр. с радиусм 3 и центром в нач. коорд.
  '''value'''
-   c_3_0_0 : Circle &equiv; (3.0, Origin)
+   c_3_0_0 : Circle == (3.0, Origin)
-'''Задача.''' Описать точку, лежащую на этой окружности
+Описать точку, лежащюю на этой окружности
-'''Решение:'''
  '''value'''
-   d_on_c_3_0_0 : Position &bull; on_circle(c_3_0_0, d_on_c_3_0_0) = True
+   d_on_c_3_0_0 : Position &dot; on_circle(c_3_0_0, d_on_c_3_0_0) = True
-'''Задача.''' Написать функцию sqrt, возвращающую значения, отличные от корня из x не более, чем на &epsilon;.
+Написать sqrt, взвр. знач, отл. от корня из x не более, чем н eps.
-'''Решение:'''
  '''value'''
-   sqrt : Real &times; Real; ⥲ Real
+   sqrt : Real &times; Real; стрелочко с тильдой Real
      sqrt(a,b) as x
-     '''post''' (abs(sqrt(a) - x) &le; b) && (x &ge; 0)
+     '''post''' (abs(sqrt(a)-x) &le; b) && (x &ge; 0)
-     '''pre''' (b &ge; 0) && (a &ge; 0)
+     '''pre''' (b ?ge; 0) && (a &ge; 0)
-'''Задача.''' Дано определение:
+Дано опр.:
  '''value'''
-   f: Int ⥲ Int
+   f: Int стрелочка с тильдой Int
-   f(x) &equiv; f(x)
+   f(x) == f(x)
-Удовлетворяет ли этому определению следующее определение:
+Удвл. ли этому опр. след. опр.:
  '''value'''
    f: Int &rarr; Int
-    f &equiv; 1, chaos, 5 — все три раза да
+    f == 1, chaos, 5 — все три раза да
-== Множества в RSL ==
+Множества в RSL
-Множество — конечный или бесконечный набор неповторяющихся элементов данного типа.
+Конеч. или беск. набор. неповт. эл-тв дного типа.
-Обозначение:
+Обозн:
  {1, 2, 3}
-В языке RSL множество определяется следующим образом:
+Опр. след. образом:
-* <tt>T - infset</tt> — для бесконечных множеств
+ T - infset #для беск.
-* <tt>T - set</tt> — для конечных множеств
+ T - set #для конечных
-Для любого типа определено пустое множество — {}.
+Для любго ипа опр. пустое мн-в — {}
-Над множеством определены следующие операции: &cap;, &cup;, &sub;, &sup;, &sube;, &supe;, &notin;, &isin;, \.
+Опр. операции: &cap;, &cuop, &sub, &ssub, &sube, &ssube, &notin;, &isin;, \
-Другие операции:
+card — рзмер множества:
+ card: T - infset стрелка с тильдоц Nat
-'''card''' — размер множества:
+ card M == |M|
- card: T - infset ⥲ Nat
- card M &equiv; |M|
  card {} = 0
- card {n|n:Nat} &equiv; chaos
+ card {n|n:Nat} == chaos
- card {1,2,3} &equiv; 3
+ card {1,2,3} == 3
-'''Примеры''':
+Примеры:
 * {"abc", "db", "efo"}
 * {1..4} = {1,2,3,4}
 * {4..1} = {}
-Такое определение множества малоприменимо на практике, поэтому обычно множества определяют через выражения и ограничения:
+Такое опр. мн-ва малоприменимо на практике, пэтому бычно мн-ва опр. через выр. и огр.:
  {expr|limit}
-'''Пример''':
+Пример:
- {2*n | n:Nat &bull; n &lt; 3} = {0, 2, 4}
+ {2*n|n:Nat &dot; n &lt; 3} = {0, 2, 4}
-'''Задача''': даны типы Student, Course, и призводные типы:
+Задача: даны типы Student, Course, и призв. типы:
  '''type''' Student, Course,
-   CourseIno = Course &times; Student-set
+   CourseIno = Course &times; Student -set
-   University =  Student-set &times; CourseInfo-set
+   University =  Student - set &times; CourseInfo - set
-Требуется:
+Задача:
-* Определить для университета множество всех студентов (функция <tt>AllStudents</tt>)
+* опр. для университета мн-во всех студентов (функция AllStudents)
-* <tt>HasCourse</tt> — курс читается в университете
+* HasCourse — курс читается в университете
-* <tt>NumberOk</tt> — каждый курс посещают не менее 5 и не более 100 человек
+* NumberOk — каждый курс посещают не менее 5 и не более 100 человек
-'''Решение:'''
  '''value'''
-   AllStudents : University &rarr; Student-set
+   AllStudents : University &rarr; Student - set
-     AllStudents ((s,ci)) &equiv; s
+     AllStudents ((s,ci)) == s
    HasCourse : Course &times; University &rarr; Bool
-     HasCourse(c,(s,ci)) &equiv; &exist; (c, si) : CourseInfo &bull; (c,si) &isin; ci
+     HasCourse(c,(s,ci)) == &exist; (c, si) : CourseInfo &dot; (c,si) &isin; ci
    NumberOk : University &rarr; Bool
-     NumberOk((s, ci)) &equiv; &forall; (c, s) : CourseInfo &bull; (((c,s) &isin; ci) &rArr; ((card s &gt; 5) &and; (card s &lt; 100)))
+     NumberOk((s, ci)) == &forall; (c, s) : CourseInfo &dot; (((c,s) &isin; ci) &rArr; ((card s &gt; 5) &and; (card s &lt; 100)))
 Почему импликация, а не конъюнкция:
  '''value'''
    c2 : Course
    u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})}
-При проверки с c=c2 получим <tt>false</tt> и значение функции <tt>false</tt>.
+При проверки с c=c2 получим false и значение функции false.
-'''Задача.''' Описать функцию <tt>StudentOf</tt>, возвращающую множество студентов, посещающих заданный курс.
+Описать функцию studentof, взвр. множество студентов, посещ. зад. курс.
-'''Решение:'''
  '''value'''
    StudentOf : Course &times; University  &rarr; Student - set
-     StudentOf(c, (s, ci)) &equiv; {st | st : Student &bull; (c_i, st) : CourseInfo &bull; ((c_i, st) &isin; ci) }
+     StudentOf(c, (s, ci)) == {st | st : Student &dot; (c_i, st) : CourseInfo &dot; ((c_i, st) &isin; ci) }
-     '''pre''' HasCourse(c, (s, ci)) &equiv; True
+     '''pre''' HasCourse(c, (s, ci)) == True
-Неявная спецификация:
+Неявная спец.:
  '''value'''
    StudentOf : Course &times; University  &rarr; Student - set
-     '''pre''' HasCourse(c, (s, ci)) &equiv; True
+     '''pre''' HasCourse(c, (s, ci)) == True
      StudentOf(c, (s, ci)) as r
      '''post'''
-       /* (r, c)  &isin; c_i — для случая, если курсы уникальны */
+       #(r, c)  &isin; c_i --- для случая, если курсы уникальный
-       &forall; (c1, ss1) : CourseIno &bull; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...
+       &orall; (c1, ss1) : CourseIno &dot; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...
-'''Задача.''' Функция, которая возвращает множество курсов, которые посещает заданный студент.
+Функция, кторая возвр. мн-ф курсов, которые псещ. заданный студент.
-'''Решение:'''
  '''value'''
    Attending : Student &times; University  &rarr; Course - set
-     Attending(s, (st, ci)) &equiv; {c | c : Course &bull; (c, st_i) : CourseInfo &bull; ((c, st_i) &isin; ci) &and; (st &isin; st_i) }
+     Attending(s, (st, ci)) == {c | c : Course &dot; (c, st_i) : CourseInfo &dot; ((c, st_i) &isin; ci) &and; (st &isin; st_i) }
-'''Задача.''' Функция newStudent, добавляющая нового студента и возвращающая обновлённый университет. DropStud — удаляет студента.
+Функция newStudent, добвл. нвог студента и взвр. обновл. университет.
+DropStud — удаляет студента
-'''Решение:'''
  '''value'''
-   NewStud : University &times; Student ⥲ University
+   NewStud : University &times; Student стрелочк с тильдой University
-     NewStud((ss, ci), s) &equiv; (ss &cup; {s}, ci)
+     NewStud((ss, ci), s) == (ss &cup; {s}, ci)
      '''pre''' s &notin; ss
-   DropStud : University &times; Student ⥲ University
+   DropStud : University &times; Student стрелочк с тильдой University
-     DropStud((ss, ci), s) &equiv; (ss \ {s}, ci_1)
+     DropStud((ss, ci), s) == (ss \ {s}, ci_1)
-     {(ss1, c) : CourseInfo &bull; (ss1 &cup; s, c) &isin; cis &and; s &notin; ss1}
+     {(ss1, c) : CourseInfo &dot; (ss1 &cup; s, c) &isin; cis &and; s &notin; ss1}
      '''pre''' s &isin; ss
-     '''post''' s &ne; ss &and; &orall; (c, ss1) : CourseInfo &bull; (c, ss1) &isin; cis &rarr; s &isin; cis
+     '''post''' s &ne; ss &and; &orall; (c, ss1) : CourseInfo &dot; (c, ss1) &isin; cis &rarr; s &isin; cis
-'''Задача.''' Удаление курса.
-'''Решение:'''
- DelCourse : University &times; Course &rarr; University
 {{МФСП}}
+{{Lection-stub}}