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

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

(Различия между версиями)
Перейти к: навигация, поиск
Строка 1: Строка 1:
-
Спи ски
+
Списки
Спискм в RSL нз. упорядч. типизир. нбр эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа
Спискм в RSL нз. упорядч. типизир. нбр эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа
Строка 8: Строка 8:
Для спискв, кк и для всех типов в rsl пр. две перации: =, ≠
Для спискв, кк и для всех типов в rsl пр. две перации: =, ≠
-
Для список опр. дв типа: T-list, T-inflist (по ANSI); T*, T^ω
+
Для список опр. дв типа: T-list, T-inflist (по ANSI); T×, T^ω
Определён пустой список: <>
Определён пустой список: <>
Строка 17: Строка 17:
Пример:
Пример:
-
<2*n|n in <0..3>>
+
<2&times;n|n in <0..3>>
Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...
Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...
Строка 29: Строка 29:
Конктенция:
Конктенция:
-
Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа
+
Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа
l1^l2
l1^l2
Строка 42: Строка 42:
Len: длина списка
Len: длина списка
len:T^&omega; стрелочк с влной Nat
len:T^&omega; стрелочк с влной Nat
-
len<n|n &dot; is_prime> == chaos
+
len<n|n &bull; is_prime> &equiv; chaos
elems: Элементы
elems: Элементы
Строка 52: Строка 52:
Задача: пр. функцию length, которя выч. длину списка
Задача: пр. функцию length, которя выч. длину списка
'''value'''
'''value'''
-
length: T* &rarr; Nat
+
length: T&times; &rarr; Nat
-
length(l) == if l &ne; <> then 1 + length(tl l) else 0 end
+
length(l) &equiv; if l &ne; <> then 1 + length(tl l) else 0 end
-
length2: T* &rarr; Nat
+
length2: T&times; &rarr; Nat
-
length2(l) == card inds l
+
length2(l) &equiv; card inds l
Конструкция case:
Конструкция case:
Строка 68: Строка 68:
Как это исп. для работы со спискми (на том же примере):
Как это исп. для работы со спискми (на том же примере):
'''value'''
'''value'''
-
length: T* &rarr; Nat
+
length: T&times; &rarr; Nat
-
length(l) ==
+
length(l) &equiv;
'''case''' l '''of'''
'''case''' l '''of'''
<> &rarr; 0
<> &rarr; 0
Строка 83: Строка 83:
'''type'''
'''type'''
-
T1={i | i:Nat &dot; i &ge; 1}
+
T1={i | i:Nat &bull; i &ge; 1}
'''value'''
'''value'''
-
pascal:T1 &rarr; (T1*)*
+
pascal:T1 &rarr; (T1&times;)&times;
-
pascal(i) == if i=1 then <<1>> else pascal(i-1)^<<1>^<pascal(i-1)(i-1)(j)+pascal(i-1)(i-1)(j-)|j:T1 &dot; j in <2..i-1>>^<1>>
+
pascal(i) &equiv; if i=1 then <<1>> else pascal(i-1)^<<1>^<pascal(i-1)(i-1)(j)+pascal(i-1)(i-1)(j-)|j:T1 &bull; j in <2..i-1>>^<1>>
Задача. Реализовать функцию rev, кторая взвр. реверсивную версию списка.
Задача. Реализовать функцию rev, кторая взвр. реверсивную версию списка.
'''value'''
'''value'''
-
rev:T* &rarr; T*
+
rev:T&times; &rarr; T&times;
-
rev(l) == if l = <> then <> else rev(tl l)^ hd l end
+
rev(l) &equiv; if l = <> then <> else rev(tl l)^ hd l end
Нерекурсивно, с пробеганием индекса
Нерекурсивно, с пробеганием индекса
'''value'''
'''value'''
-
rev:T* &rarr; T*
+
rev:T&times; &rarr; T&times;
-
rev(l) == <l(len(l)+1-n)|n in <1..len(n)>>
+
rev(l) &equiv; <l(len(l)+1-n)|n in <1..len(n)>>
Даны следующие типы:
Даны следующие типы:
'''type'''
'''type'''
-
Page=Line*,
+
Page=Line&times;,
-
Line=Word*,
+
Line=Word&times;,
Word
Word
-
(стандартный тип text в rsl н смом деле text=char*)
+
(стандартный тип text в rsl н смом деле text=char&times;)
Для тких типов тр. опр. функцию is_on, проверяющую, встречется ли данне слово на странице
Для тких типов тр. опр. функцию is_on, проверяющую, встречется ли данне слово на странице
Строка 113: Строка 113:
'''value'''
'''value'''
is_on: Word &times; Page &rarr; Bool
is_on: Word &times; Page &rarr; Bool
-
is_on(w,p) == if p=<> then False else w &isin; elems hd p &or; is_on(w, tl p) end
+
is_on(w,p) &equiv; if p=<> then False else w &isin; elems hd p &or; is_on(w, tl p) end
-
 
+
is_on: Word &times; Page &rarr; Bool
is_on: Word &times; Page &rarr; Bool
-
is_on(w,p) == &exist; i : Nat &dot; (i &isin; {1..len(p)}) &and; (w &isin; elems p(i))
+
is_on(w,p) &equiv; &exist; i : Nat &bull; (i &isin; {1..len(p)}) &and; (w &isin; elems p(i))
Определить number_of, пдсчитывающую количество вхождений слоов в страницу
Определить number_of, пдсчитывающую количество вхождений слоов в страницу
Строка 123: Строка 123:
number_of: Word &times; Page &rarr; Nat
number_of: Word &times; Page &rarr; Nat
number_of(w,p) &rarr; if p=<> then 0 else number_of_line(w,l) + number_of(w, tl p)
number_of(w,p) &rarr; if p=<> then 0 else number_of_line(w,l) + number_of(w, tl p)
-
 
+
number_of_line: Word &times; Line &rarr; Nat
number_of_line: Word &times; Line &rarr; Nat
number_o_line(w,l) &rarr; if l=<> then 0 else (if w=hd l then 1 else 0) + number_of_line(w, tl l)
number_o_line(w,l) &rarr; if l=<> then 0 else (if w=hd l then 1 else 0) + number_of_line(w, tl l)
Строка 129: Строка 129:
number_of: Word &times; Page &rarr; Nat
number_of: Word &times; Page &rarr; Nat
-
number_of(w,p) &rarr; {(i,j)|(i:Nat&dot;j:Nat; &dot; p(i)(j)=w &and; i&isin; p &and; &isin;p(i)}
+
number_of(w,p) &rarr; {(i,j)|(i:Nat&bull;j:Nat; &bull; p(i)(j)=w &and; i&isin; p &and; &isin;p(i)}
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

Версия 15:33, 4 октября 2008

Списки

Спискм в RSL нз. упорядч. типизир. нбр эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа

<1, 3, 1, 5, 4>
<false, true>

Для спискв, кк и для всех типов в rsl пр. две перации: =, ≠

Для список опр. дв типа: T-list, T-inflist (по ANSI); T×, T^ω

Определён пустой список: <>

пр. синтаксис <v1..vn>

Опр. синтксис: <expr|limit>

Пример:

<2×n|n in <0..3>>

Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...

Для того, чтобы добрться д эл-та, исп. перация index, "()", в которой ук. номер эл-та:

<1,4,5,6>(2) = 4
<2,5,3>,<3,1>>(2) = <3,1>
<2,5,3>,<3,1>>(2)(2) = 1

Операции со списками:

Конктенция: Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа

l1^l2

Head: Первый элемент

hd: T^ω стрелочк с влной T
hd<> = chaos

Tail: Хвст

tl: T^ω стрпелчк с волной T^ω
tl<> = chaos

Len: длина списка

len:T^ω стрелочк с влной Nat
len<n|n • is_prime> ≡ chaos

elems: Элементы

elems: T^ω стрелочк с волнлй T-infset

inds: Индексы

inds: T^ω стрелочк с волнлй Nat-infset 

Задача: пр. функцию length, которя выч. длину списка

value
  length: T× → Nat
    length(l) ≡ if l ≠ <> then 1 + length(tl l) else 0 end
  length2: T× → Nat 
    length2(l) ≡ card inds l

Конструкция case:

case cond of
  pattern1expr1
  pattern2expr2
  ...
  _ → def_expr
end

Как это исп. для работы со спискми (на том же примере):

value
  length: T× → Nat
    length(l) ≡
      case l of
        <> → 0
        <i>^lr → length(lr) + 1
      end

Задач. Опр. функцию Pascal, гненер. тр. Пскаля д урвня n вкл. Результат --- список списков. Например:

<<1>,
 <1,1>,
 <1,2,1>,
 <1,3,3,1>,
 <1,4,6,4,1>>
type
  T1={i | i:Nat • i ≥ 1}

value
  pascal:T1 → (T1×)×
    pascal(i) ≡ if i=1 then <<1>> else pascal(i-1)^<<1>^<pascal(i-1)(i-1)(j)+pascal(i-1)(i-1)(j-)|j:T1 • j in <2..i-1>>^<1>>

Задача. Реализовать функцию rev, кторая взвр. реверсивную версию списка.

value
  rev:T× → T×
    rev(l) ≡ if l = <> then <> else rev(tl l)^ hd l end

Нерекурсивно, с пробеганием индекса

value
  rev:T× → T×
    rev(l) ≡ <l(len(l)+1-n)|n in <1..len(n)>>

Даны следующие типы:

type
  Page=Line×,
  Line=Word×,
  Word

(стандартный тип text в rsl н смом деле text=char×)

Для тких типов тр. опр. функцию is_on, проверяющую, встречется ли данне слово на странице

value
  is_on: Word × Page → Bool
    is_on(w,p) ≡ if p=<> then False else w ∈ elems hd p ∨ is_on(w, tl p) end

  is_on: Word × Page → Bool
    is_on(w,p) ≡ ∃ i : Nat • (i ∈ {1..len(p)}) ∧ (w ∈ elems p(i))

Определить number_of, пдсчитывающую количество вхождений слоов в страницу

value
  number_of: Word × Page → Nat
    number_of(w,p) → if p=<> then 0 else number_of_line(w,l) + number_of(w, tl p)

  number_of_line: Word × Line → Nat
    number_o_line(w,l) → if l=<> then 0 else (if w=hd l then 1 else 0) + number_of_line(w, tl l)


  number_of: Word × Page → Nat
    number_of(w,p) → {(i,j)|(i:Nat•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)}


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


Лекции

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

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


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

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