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

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

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

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

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

Даны типы:

type position = Real×Real;
value
  origin : Position = (0.0, 0.0) # начло координат
  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

определить: тип circle, функцию on_circle

type
  Circle = Real × Position # радиус, центр
value
  on_circle : Circle × Position → 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 • on_circle(c_3_0_0, d_on_c_3_0_0) = True

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

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

Дано опр.:

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

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

value
  f: Int → Int
   f ≡ 1, chaos, 5 — все три раза да

Множества в RSL

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

Обозн:

{1, 2, 3}

Опр. след. образом:

T - infset #для беск.
T - set #для конечных

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

Опр. операции: ∩, &cuop, &sub, &ssub, &sube, &ssube, ∉, ∈, \

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 • n < 3} = {0, 2, 4}

Задача: даны типы Student, Course, и призв. типы:

type Student, Course, 
  CourseIno = Course × Student -set
  University =  Student - set × CourseInfo - set

Задача:

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

value
  AllStudents : University → Student - set
    AllStudents ((s,ci)) ≡ s
  HasCourse : Course × University → Bool
    HasCourse(c,(s,ci)) ≡ ∃ (c, si) : CourseInfo • (c,si) ∈ ci
  NumberOk : University → Bool
    NumberOk((s, ci)) ≡ ∀ (c, s) : CourseInfo • (((c,s) ∈ ci) ⇒ ((card s > 5) ∧ (card s < 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 × University  → Student - set
    StudentOf(c, (s, ci)) ≡ {st | st : Student • (c_i, st) : CourseInfo • ((c_i, st) ∈ ci) }
    pre HasCourse(c, (s, ci)) ≡ True

Неявная спец.:

value
  StudentOf : Course × University  → Student - set
    pre HasCourse(c, (s, ci)) ≡ True
    StudentOf(c, (s, ci)) as r
    post 
      #(r, c)  ∈ c_i --- для случая, если курсы уникальный
      &orall; (c1, ss1) : CourseIno • (c1, ss1) ∈ ci ∧ r &ssub; ss1 ∧ ...

Функция, кторая возвр. мн-ф курсов, которые псещ. заданный студент.

value
  Attending : Student × University  → Course - set
    Attending(s, (st, ci)) ≡ {c | c : Course • (c, st_i) : CourseInfo • ((c, st_i) ∈ ci) ∧ (st ∈ st_i) }

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

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

value 
  NewStud : University × Student стрелочк с тильдой University
    NewStud((ss, ci), s) ≡ (ss ∪ {s}, ci)
    pre s ∉ ss

  DropStud : University × Student стрелочк с тильдой University
    DropStud((ss, ci), s) ≡ (ss \ {s}, ci_1) 
    {(ss1, c) : CourseInfo • (ss1 ∪ s, c) ∈ cis ∧ s ∉ ss1}
    pre s ∈ ss
    post s ≠ ss ∧ &orall; (c, ss1) : CourseInfo • (c, ss1) ∈ cis → s ∈ cis