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

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

(Различия между версиями)
Перейти к: навигация, поиск
Строка 1: Строка 1:
-
Продолжаем изучть язык RSL
+
В прошлый раз рассматривались типы, операции с ними, производные типы. Разобрались с функциями, константами.
-
 
+
-
В прошлый раз рассм. типы, операции с ними, призв. типы. Разбрались с функц., кнстантами.
+
Сейчас: дорешать задачи пр функции и перейти к множествам.
Сейчас: дорешать задачи пр функции и перейти к множествам.
-
Даны типы:
 
 +
'''Задача.''' Даны типы:
'''type''' position = Real×Real;
'''type''' position = Real×Real;
'''value'''
'''value'''
-
origin : Position = (0.0, 0.0) # начло координат
+
origin : Position = (0.0, 0.0) /* начало координат */
dist : Position × Position → Real
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
dist((x_1, y_1), (x_2, y_2)) ≡ ((x_1 - x_2)^2.0 + (y_1 - y_2)^2.0)^0.5
Строка 15: Строка 13:
определить: тип circle, функцию on_circle
определить: тип circle, функцию on_circle
 +
'''Решение:'''
'''type'''
'''type'''
Circle = Real × Position # радиус, центр
Circle = Real × Position # радиус, центр
Строка 21: Строка 20:
on_circle((r, c_0), c) ≡ (dist(c_0, c) = r)
on_circle((r, c_0), c) ≡ (dist(c_0, c) = r)
-
Описать окр. с радиусм 3 и центром в нач. коорд.
+
'''Задача.''' Описать окружность с радиусом 3 и центром в начале координат.
'''value'''
'''value'''
c_3_0_0 : Circle ≡ (3.0, Origin)
c_3_0_0 : Circle ≡ (3.0, Origin)
-
Описать точку, лежащюю на этой окружности
+
'''Задача.''' Описать точку, лежащую на этой окружности
 +
'''Решение:'''
'''value'''
'''value'''
d_on_c_3_0_0 : Position • on_circle(c_3_0_0, d_on_c_3_0_0) = True
d_on_c_3_0_0 : Position • on_circle(c_3_0_0, d_on_c_3_0_0) = True
-
Написать sqrt, взвр. знач, отл. от корня из x не более, чем н eps.
+
'''Задача.''' Написать функцию sqrt, возвращающую значения, отличные от корня из x не более, чем на ε.
 +
'''Решение:'''
'''value'''
'''value'''
-
sqrt : Real × Real; стрелочко с тильдой Real
+
sqrt : Real × Real; Real
sqrt(a,b) as x
sqrt(a,b) as x
-
'''post''' (abs(sqrt(a)-x) ≤ b) && (x ≥ 0)
+
'''post''' (abs(sqrt(a) - x) ≤ b) && (x ≥ 0)
-
'''pre''' (b ?ge; 0) && (a ≥ 0)
+
'''pre''' (b ≥ 0) && (a ≥ 0)
-
Дано опр.:
+
'''Задача.''' Дано определение:
'''value'''
'''value'''
-
f: Int стрелочка с тильдой Int
+
f: Int Int
f(x) ≡ f(x)
f(x) ≡ f(x)
-
Удвл. ли этому опр. след. опр.:
+
Удовлетворяет ли этому определению следующее определение:
'''value'''
'''value'''

Версия 08:36, 29 сентября 2010

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

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


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

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

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


Эта статья является конспектом лекции.

Эта статья ещё не вычитана. Пожалуйста, вычитайте её и исправьте ошибки, если они есть.
Личные инструменты
Разделы