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

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

Версия от 05:55, 27 сентября 2010; 212.192.248.201 (Обсуждение)

(разн.) ← Предыдущая | Текущая версия (разн.) | Следующая → (разн.)

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

Внимание: Вы не представились системе. Ваш 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)) &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 не более, чем н 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) &equiv; f(x)

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

'''value'''
   f: Int &rarr; Int
    f &equiv; 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 &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

Задача: 
* опр. для университета мн-во всех студентов (функция AllStudents)
* HasCourse — курс читается в университете
* NumberOk — каждый курс посещают не менее 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 получим false и значение функции false.

Описать функцию 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) }
     '''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 --- для случая, если курсы уникальный
       &orall; (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''' 
   <math>NewStud : University\times Student\overset{\sim}{\rightarrow}University</math> 
     NewStud((ss, ci), s) &equiv; (ss &cup; {s}, ci)
     '''pre''' s &notin; ss

DropStud : University &times; Student <math>\overset{\sim}{\rightarrow}</math> 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

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

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

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

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

Получено с http://esyr.name/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