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

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

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

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

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

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

'''Задача.''' Даны типы:
 '''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)) &equiv; ((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)

'''Задача.''' Описать окружность с радиусом 3 и центром в начале координат.

'''value'''
   c_3_0_0 : Circle &equiv; (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

'''Задача.''' Написать функцию sqrt, возвращающую значения, отличные от корня из x не более, чем на &epsilon;.

'''Решение:'''
 '''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) &equiv; f(x)

Удовлетворяет ли этому определению следующее определение:

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

== Множества в RSL ==

Множество — конечный или бесконечный набор неповторяющихся элементов данного типа.

Обозначение: 
 {1, 2, 3}

В языке RSL множество определяется следующим образом:
* <tt>T - infset</tt> — для бесконечных множеств
* <tt>T - set</tt> — для конечных множеств

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

Над множеством определены следующие операции: &cap;, &cup;, &sub;, &sup;, &sube;, &supe;, &notin;, &isin;, \.

Другие операции:

'''card''' — размер множества:
 card: T - infset ⥲ Nat
 card M &equiv; |M|

card {} = 0
 card {n|n:Nat} &equiv; chaos
 card {1,2,3} &equiv; 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}

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

Требуется: 
* Определить для университета множество всех студентов (функция <tt>AllStudents</tt>)
* <tt>HasCourse</tt> — курс читается в университете
* <tt>NumberOk</tt> — каждый курс посещают не менее 5 и не более 100 человек

'''Решение:'''
 '''value'''
   AllStudents : University &rarr; Student-set
     AllStudents ((s,ci)) &equiv; s
   HasCourse : Course &times; University &rarr; Bool
     HasCourse(c,(s,ci)) &equiv; &exist; (c, si) : CourseInfo &bull; (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)))

Почему импликация, а не конъюнкция:
 '''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>.

'''Задача.''' Описать функцию <tt>StudentOf</tt>, возвращающую множество студентов, посещающих заданный курс.

'''Решение:'''
 '''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) }
     '''pre''' HasCourse(c, (s, ci)) &equiv; True

Неявная спецификация:
 '''value'''
   StudentOf : Course &times; University  &rarr; Student - set
     '''pre''' HasCourse(c, (s, ci)) &equiv; True
     StudentOf(c, (s, ci)) as r
     '''post''' 
       /* (r, c)  &isin; c_i — для случая, если курсы уникальны */
       &forall; (c1, ss1) : CourseIno &bull; (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) }

'''Задача.''' Функция newStudent, добавляющая нового студента и возвращающая обновлённый университет. DropStud — удаляет студента.

'''Решение:'''
 '''value''' 
   NewStud : University &times; Student ⥲ University
     NewStud((ss, ci), s) &equiv; (ss &cup; {s}, ci)
     '''pre''' s &notin; ss

DropStud : University &times; Student ⥲ University
     DropStud((ss, ci), s) &equiv; (ss \ {s}, ci_1) 
     {(ss1, c) : CourseInfo &bull; (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

'''Задача.''' Удаление курса.

'''Решение:'''
 DelCourse : University &times; Course &rarr; University

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. 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: @@
 В прошлый раз рассматривались типы, операции с ними, производные типы. Разобрались с функциями, константами.
-Сейчас: дорешать задачи про функции и перейти к множествам.
+Сейчас: дорешать задачи пр функции и перейти к множествам.
@@ Строка 131: / Строка 131: @@
        &forall; (c1, ss1) : CourseIno &bull; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...
-'''Задача.''' Функция, которая возвращает множество курсов, которые посещает заданный студент.
+'''Задача.''' Функция, кторая возвращает множество курсов, которые посещает заданный студент.
 '''Решение:'''