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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Множества в RSL)
м
 
(4 промежуточные версии не показаны)
Строка 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'''
Строка 53: Строка 54:
== Множества в RSL ==
== Множества в RSL ==
-
Конеч. или беск. набор. неповт. эл-тв дного типа.
+
Множество — конечный или бесконечный набор неповторяющихся элементов данного типа.
-
Обозн:
+
Обозначение:
{1, 2, 3}
{1, 2, 3}
-
Опр. след. образом:
+
В языке RSL множество определяется следующим образом:
-
T - infset #для беск.
+
* <tt>T - infset</tt> — для бесконечных множеств
-
T - set #для конечных
+
* <tt>T - set</tt> — для конечных множеств
-
Для любго ипа опр. пустое мн-в — {}
+
Для любого типа определено пустое множество — {}.
-
Опр. операции: &cap;, &cuop, &sub, &ssub, &sube, &ssube, &notin;, &isin;, \
+
Над множеством определены следующие операции: &cap;, &cup;, &sub;, &sup;, &sube;, &supe;, &notin;, &isin;, \.
-
card — рзмер множества:
+
Другие операции:
-
card: T - infset стрелка с тильдоц Nat
+
 
 +
'''card''' размер множества:
 +
card: T - infset Nat
card M &equiv; |M|
card M &equiv; |M|
Строка 74: Строка 77:
card {1,2,3} &equiv; 3
card {1,2,3} &equiv; 3
-
Примеры:
+
'''Примеры''':
* {"abc", "db", "efo"}
* {"abc", "db", "efo"}
* {1..4} = {1,2,3,4}
* {1..4} = {1,2,3,4}
* {4..1} = {}
* {4..1} = {}
-
Такое опр. мн-ва малоприменимо на практике, пэтому бычно мн-ва опр. через выр. и огр.:
+
Такое определение множества малоприменимо на практике, поэтому обычно множества определяют через выражения и ограничения:
{expr|limit}
{expr|limit}
-
Пример:
+
'''Пример''':
-
{2*n|n:Nat &bull; n &lt; 3} = {0, 2, 4}
+
{2*n | n:Nat &bull; n &lt; 3} = {0, 2, 4}
-
Задача: даны типы Student, Course, и призв. типы:
+
'''Задача''': даны типы Student, Course, и призводные типы:
'''type''' Student, Course,
'''type''' Student, Course,
-
CourseIno = Course &times; Student -set
+
CourseIno = Course &times; Student-set
-
University = Student - set &times; CourseInfo - set
+
University = Student-set &times; CourseInfo-set
-
Задача:
+
Требуется:
-
* опр. для университета мн-во всех студентов (функция AllStudents)
+
* Определить для университета множество всех студентов (функция <tt>AllStudents</tt>)
-
* HasCourse — курс читается в университете
+
* <tt>HasCourse</tt> — курс читается в университете
-
* NumberOk — каждый курс посещают не менее 5 и не более 100 человек
+
* <tt>NumberOk</tt> — каждый курс посещают не менее 5 и не более 100 человек
 +
'''Решение:'''
'''value'''
'''value'''
-
AllStudents : University &rarr; Student - set
+
AllStudents : University &rarr; Student-set
AllStudents ((s,ci)) &equiv; s
AllStudents ((s,ci)) &equiv; s
HasCourse : Course &times; University &rarr; Bool
HasCourse : Course &times; University &rarr; Bool
Строка 104: Строка 108:
Почему импликация, а не конъюнкция:
Почему импликация, а не конъюнкция:
- 
'''value'''
'''value'''
c2 : Course
c2 : Course
u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})}
u : University = {{s1, s2, s3, s4, s5, s6}, (c1, {s1, s2, s3, s4, s5, s6})}
-
При проверки с c=c2 получим false и значение функции false.
+
При проверки с c=c2 получим <tt>false</tt> и значение функции <tt>false</tt>.
-
Описать функцию studentof, взвр. множество студентов, посещ. зад. курс.
+
'''Задача.''' Описать функцию <tt>StudentOf</tt>, возвращающую множество студентов, посещающих заданный курс.
 +
'''Решение:'''
'''value'''
'''value'''
StudentOf : Course &times; University &rarr; Student - set
StudentOf : Course &times; University &rarr; Student - set
Строка 118: Строка 122:
'''pre''' HasCourse(c, (s, ci)) &equiv; True
'''pre''' HasCourse(c, (s, ci)) &equiv; True
-
Неявная спец.:
+
Неявная спецификация:
'''value'''
'''value'''
StudentOf : Course &times; University &rarr; Student - set
StudentOf : Course &times; University &rarr; Student - set
Строка 124: Строка 128:
StudentOf(c, (s, ci)) as r
StudentOf(c, (s, ci)) as r
'''post'''
'''post'''
-
#(r, c) &isin; c_i --- для случая, если курсы уникальный
+
/* (r, c) &isin; c_i для случая, если курсы уникальны */
-
&orall; (c1, ss1) : CourseIno &bull; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...
+
&forall; (c1, ss1) : CourseIno &bull; (c1, ss1) &isin; ci &and; r &ssub; ss1 &and; ...
-
Функция, кторая возвр. мн-ф курсов, которые псещ. заданный студент.
+
'''Задача.''' Функция, которая возвращает множество курсов, которые посещает заданный студент.
 +
 
 +
'''Решение:'''
'''value'''
'''value'''
Attending : Student &times; University &rarr; Course - set
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) }
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, добвл. нвог студента и взвр. обновл. университет.
+
'''Задача.''' Функция newStudent, добавляющая нового студента и возвращающая обновлённый университет. DropStud — удаляет студента.
-
 
+
-
DropStud — удаляет студента
+
 +
'''Решение:'''
'''value'''
'''value'''
-
<math>NewStud : University\times Student\overset{\sim}{\rightarrow}University</math>
+
NewStud : University &times; Student University
NewStud((ss, ci), s) &equiv; (ss &cup; {s}, ci)
NewStud((ss, ci), s) &equiv; (ss &cup; {s}, ci)
'''pre''' s &notin; ss
'''pre''' s &notin; ss
-
DropStud : University &times; Student <math>\overset{\sim}{\rightarrow}</math> University
+
DropStud : University &times; Student University
DropStud((ss, ci), s) &equiv; (ss \ {s}, ci_1)
DropStud((ss, ci), s) &equiv; (ss \ {s}, ci_1)
{(ss1, c) : CourseInfo &bull; (ss1 &cup; s, c) &isin; cis &and; s &notin; ss1}
{(ss1, c) : CourseInfo &bull; (ss1 &cup; s, c) &isin; cis &and; s &notin; ss1}
'''pre''' s &isin; ss
'''pre''' s &isin; ss
'''post''' s &ne; ss &and; &orall; (c, ss1) : CourseInfo &bull; (c, ss1) &isin; cis &rarr; s &isin; cis
'''post''' s &ne; ss &and; &orall; (c, ss1) : CourseInfo &bull; (c, ss1) &isin; cis &rarr; s &isin; cis
 +
 +
'''Задача.''' Удаление курса.
 +
 +
'''Решение:'''
 +
DelCourse : University &times; Course &rarr; University
{{МФСП}}
{{МФСП}}
-
{{Lection-stub}}
 

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

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

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


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

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

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


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