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

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

Текущая версия

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

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

Задача. Даны типы:

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 не более, чем на ε.

Решение:

value
  sqrt : Real × Real; ⥲ Real
    sqrt(a,b) as x
    post (abs(sqrt(a) - x) ≤ b) && (x ≥ 0)
    pre (b ≥ 0) && (a ≥ 0)

Задача. Дано определение:

value
  f: Int ⥲ Int
  f(x) ≡ f(x)

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

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

[править] Множества в RSL

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

Обозначение:

{1, 2, 3}

В языке RSL множество определяется следующим образом:

• T - infset — для бесконечных множеств
• T - set — для конечных множеств

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

Над множеством определены следующие операции: ∩, ∪, ⊂, ⊃, ⊆, ⊇, ∉, ∈, \.

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

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 — для случая, если курсы уникальны */
      ∀ (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

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

Решение:

DelCourse : University × Course → University