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

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

(Различия между версиями)
Перейти к: навигация, поиск
(<math>\tilde\rightarrow</math>)
 
(24 промежуточные версии не показаны)
Строка 1: Строка 1:
-
Спи ски
+
=Списки=
-
Спискм в RSL нз. упорядч. типизир. нбр эл-тов, эл-иы могут пвторяться. Списк в угловых скбкх, прядок вжен, все элементы дного типа
+
Списки в RSL — упорядоченный типизированный набор элементов, элементы могут повторяться. Список в угловых скобках, порядок важен, все элементы одного типа
<1, 3, 1, 5, 4>
<1, 3, 1, 5, 4>
<false, true>
<false, true>
-
Для спискв, кк и для всех типов в rsl пр. две перации: =, &ne;
+
Для списков, как и для всех типов в rsl определены две операции: =, &ne;
-
Для список опр. дв типа: T-list, T-inflist (по ANSI); T*, T^&omega;
+
Для списков определено два типа: T-list(для конечных), T-inflist(для бесконечных) (по ANSI); T&times;, T^&omega;
Определён пустой список: <>
Определён пустой список: <>
Строка 14: Строка 14:
пр. синтаксис <v1..vn>
пр. синтаксис <v1..vn>
-
Опр. синтксис: <expr|limit>
+
Опр. синтаксис: <expr|limit>
Пример:
Пример:
-
<2*n|n in <0..3>>
+
<2&times;n|n in <0..3>>
-
Список может быть опр. для лдюбго ип, не олько бзового: мнжества, списка...
+
<3..7> &equiv; < 3,4,5,6,7>
 +
<7..3 > &equiv; <>
-
Для того, чтобы добрться д эл-та, исп. перация index, "()", в которой ук. номер эл-та:
+
Список может быть определён для любого типа, не только базового: множества, списка...
 +
 
 +
==Индексация==
 +
 
 +
Для того, чтобы добраться до элемента, используется операция index, "()", в которой указан номер элемента:
<1,4,5,6>(2) = 4
<1,4,5,6>(2) = 4
<2,5,3>,<3,1>>(2) = <3,1>
<2,5,3>,<3,1>>(2) = <3,1>
<2,5,3>,<3,1>>(2)(2) = 1
<2,5,3>,<3,1>>(2)(2) = 1
 +
 +
Если по не существующему номеру, то возвращает chaos.
Операции со списками:
Операции со списками:
-
Конктенция:
+
===Конкатенация===
-
Конк. мжно применять только к кнеч. спискм, второй эл-т мжет быть и конеч, и беск. Рез-т соотв. типа
+
Конкатенацию можно применять только к конечным спискам, второй элемент может быть и конечным, и бесконечным. Результат соответствующего типа
l1^l2
l1^l2
 +
^:T-list x T-inflist -> T-inflist
Head: Первый элемент
Head: Первый элемент
-
hd: T^&omega; стрелочк с влной T
+
hd: T^&omega; <math>\tilde\rightarrow</math> T
hd<> = chaos
hd<> = chaos
-
Tail: Хвст
+
Tail: Хвост
-
tl: T^&omega; стрпелчк с волной T^&omega;
+
tl: T^&omega; <math>\tilde\rightarrow</math> T^&omega;
tl<> = chaos
tl<> = chaos
Len: длина списка
Len: длина списка
-
len:T^&omega; стрелочк с влной Nat
+
len:T^&omega; <math>\tilde\rightarrow</math> Nat
-
len<n|n &dot; is_prime> == chaos
+
len<n|n &bull; is_prime> &equiv; chaos
-
elems: Элементы
+
===elems: Элементы===
-
elems: T^&omega; стрелочк с волнлй T-infset
+
elems: T^&omega; <math>\tilde\rightarrow</math> T-infset
 +
Возвращает множество элементов списка
-
inds: Индексы
+
===inds: Индексы===
-
inds: T^&omega; стрелочк с волнлй Nat-infset
+
inds: T^&omega; <math>\tilde\rightarrow</math> Nat-infset
 +
inds FL={1..len FL}
-
Задача: пр. функцию 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:
Конструкция case:
'''case''' ''cond'' '''of'''
'''case''' ''cond'' '''of'''
Строка 66: Строка 78:
'''end'''
'''end'''
-
Как это исп. для работы со спискми (на том же примере):
+
===Список чисел Фибоначчи===
 +
type Nat1= {n:Nat &circle; n > 0 }
 +
value Fib:Nat1->Nat1
 +
Fib(n) &equiv;
 +
case n of
 +
1->1
 +
2->2
 +
_->Fib(n-2)+Fib(n-1)
 +
end
 +
 
 +
=== ===
 +
'''value''' rev:int-list&times; &rarr; T&times;
 +
rev(l) &equiv;
 +
case L of
 +
<> -> <>
 +
<_i>^L2 -> rev(L2)^<_i>
 +
end
 +
 
 +
 
 +
Как это используется для работы со списками (на том же примере):
'''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
Строка 75: Строка 106:
'''end'''
'''end'''
-
Задач. Опр. функцию Pascal, гненер. тр. Пскаля д урвня n вкл. Результат --- список списков. Например:
+
Задача. Определить функцию Pascal, генерирующую треугольник Паскаля до уровня n включительно. Результат --- список списков. Например:
<<1>,
<<1>,
<1,1>,
<1,1>,
Строка 83: Строка 114:
'''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, проверяющую, встречается ли данне слово на странице
'''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, подсчитывающую количество вхождений слов в страницу
'''value'''
'''value'''
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: Строка 160:
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; card {(i,j)|(i:Nat&bull;j:Nat; &bull; p(i)(j)=w &and; i&isin; p &and; &isin;p(i)}
 +
 
 +
=== еще задачки ===
 +
является упорядоченным?
 +
value isStore: Int-list &right; bool
 +
isStore(l)= &forall; i:int &bull; i >= 1; &and; i < len(l) => l(i+1) > l(i)
 +
 
 +
==== длина списка ====
 +
value len2: Elem-list-> Nat
 +
len2(E) &equal; ( if (E=<>) then 0 else 1+len2(tl E ) end )
 +
 
 +
len3(E) - card inds E
 +
==== удаляем заданный элем-т из списка ====
 +
value del: E-list &times; E &rarr; E-list
 +
del(l, x): &equal; < E(i) | i in <1..len L > &bull; L(i) != x >
 +
 
 +
==== подсчет ====
 +
value numOf: E-list &times; E -> Int
 +
NumberOf(L,x) = if ( LL=<> ) then 0 else
 +
if( hd(L) = x ) then NumberOf( tl L, x ) +1 else NumberOf( tl L, x)
 +
 
 +
==отображения==
 +
<math>[3 \rightarrow , 5 \rightarrow false](1) = chaos</math>
 +
 
 +
операция взятия домена
 +
 
 +
<math>dom:(T[d] \overset{m}{\rightarrow} T[r] ) \rightarrow T[d]-infset</math>
 +
<math>rng:(T[A] \overset{m}{\rightarrow} T[r] ) \rightarrow T[r]-infset</math>
{{МФСП}}
{{МФСП}}
{{Lection-stub}}
{{Lection-stub}}

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

Содержание

[править] Списки

Списки в 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>>
<3..7> ≡ < 3,4,5,6,7>
<7..3 > ≡ <>

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

[править] Индексация

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

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

Если по не существующему номеру, то возвращает chaos.

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

[править] Конкатенация

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

l1^l2
^:T-list x T-inflist -> T-inflist

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

hd: T^ω \tilde\rightarrow T
hd<> = chaos

Tail: Хвост

tl: T^ω \tilde\rightarrow T^ω
tl<> = chaos

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

len:T^ω \tilde\rightarrow Nat
len<n|n • is_prime> ≡ chaos

[править] elems: Элементы

elems: T^ω \tilde\rightarrow T-infset
Возвращает множество элементов списка

[править] inds: Индексы

inds: T^ω \tilde\rightarrow Nat-infset 
inds FL={1..len FL}

[править] Задача

Задача: пр. функцию 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:

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

[править] Список чисел Фибоначчи

type Nat1= {n:Nat &circle; n > 0 }
value Fib:Nat1->Nat1
      Fib(n) ≡  
case n of  
      1->1
      2->2
      _->Fib(n-2)+Fib(n-1)
end

[править]

value rev:int-list× → T×
    rev(l) ≡ 
case L of 
<> -> <> 
<_i>^L2 -> rev(L2)^<_i>
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) → card {(i,j)|(i:Nat•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)}

[править] еще задачки

является упорядоченным?

value isStore: Int-list &right; bool
isStore(l)= ∀ i:int • i >= 1; ∧ i < len(l) => l(i+1) > l(i)

[править] длина списка

value len2: Elem-list-> Nat
len2(E) &equal; ( if (E=<>) then 0 else 1+len2(tl E ) end )
len3(E) - card inds E

[править] удаляем заданный элем-т из списка

value del: E-list × E → E-list
      del(l, x): &equal; < E(i) | i in <1..len L > • L(i) != x >

[править] подсчет

value numOf: E-list × E -> Int
NumberOf(L,x) = if ( LL=<> ) then 0 else
    if( hd(L) = x ) then NumberOf( tl L, x ) +1 else NumberOf( tl L, x)

[править] отображения

[3 \rightarrow , 5 \rightarrow false](1) = chaos

операция взятия домена

dom:(T[d] \overset{m}{\rightarrow} T[r] ) \rightarrow T[d]-infset

rng:(T[A] \overset{m}{\rightarrow} T[r] ) \rightarrow T[r]-infset

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


Лекции

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

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


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

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