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

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

(Различия между версиями)
Перейти к: навигация, поиск
(Множества в RSL)
Строка 137: Строка 137:
'''value'''
'''value'''
-
NewStud : University × Student стрелочк с тильдой University
+
<math>NewStud : University\times Student\overset{\sim}{\rightarrow}University</math>
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 стрелочк с тильдой University
+
DropStud : University &times; Student <math>\overset{\sim}{\rightarrow}</math> 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}

Версия 05:55, 27 сентября 2010

Продолжаем изучть язык RSL

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

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

Даны типы:

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

value
  sqrt : Real × Real; стрелочко с тильдой Real
    sqrt(a,b) as x
    post (abs(sqrt(a)-x) ≤ b) && (x ≥ 0)
    pre (b ?ge; 0) && (a ≥ 0)

Дано опр.:

value
  f: Int стрелочка с тильдой Int
  f(x) ≡ f(x)

Удвл. ли этому опр. след. опр.:

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

Множества в RSL

Конеч. или беск. набор. неповт. эл-тв дного типа.

Обозн:

{1, 2, 3}

Опр. след. образом:

T - infset #для беск.
T - set #для конечных

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

Опр. операции: ∩, &cuop, &sub, &ssub, &sube, &ssube, ∉, ∈, \

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 --- для случая, если курсы уникальный
      &orall; (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\times Student\overset{\sim}{\rightarrow}University 
    NewStud((ss, ci), s) ≡ (ss ∪ {s}, ci)
    pre s ∉ ss
  DropStud : University × Student \overset{\sim}{\rightarrow} 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


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


Лекции

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

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


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

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