МФСП, 04 семинар (от 22 сентября)
Материал из eSyr's wiki.
(→удаляем заданный элем-т из списка) |
(→) |
||
| Строка 160: | Строка 160: | ||
number_of: Word × Page → Nat | number_of: Word × Page → Nat | ||
| - | number_of(w,p) → {(i,j)|(i:Nat•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)} | + | number_of(w,p) → card {(i,j)|(i:Nat•j:Nat; • p(i)(j)=w ∧ i∈ p ∧ ∈p(i)} |
| - | + | ||
| - | + | ||
=== еще задачки === | === еще задачки === | ||
Версия 05:32, 4 октября 2010
Содержание |
Списки
Списки в 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^ω стрелочка с волной 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
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 pattern1 → expr1 pattern2 → expr2 ... _ → 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)
Формальная спецификация и верификация программ
|
|
