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

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

Версия 08:30, 29 сентября 2010 (править) ESyr01 (Обсуждение | вклад) ← К предыдущему изменению		Версия 08:36, 29 сентября 2010 (править) (отменить) ESyr01 (Обсуждение | вклад) К следующему изменению →
Строка 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