МФСП, 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


Формальная спецификация и верификация программ


Лекции

01 02 03 04 05 06 07 08 09 10 11 12 13 14


Календарь

Сентябрь
03 10 17 24
Октябрь
01 08 15 22 29
Ноябрь
12 19 26
Декабрь
03 17
Семинары

01 02 03 04 05 06


Календарь

Сентябрь
01 08 15 22 29
Октябрь
06

Оформление задач|Проведение экзамена


Эта статья является конспектом лекции.
Личные инструменты
Разделы