МФСП, 04 семинар (от 22 сентября)
Материал из eSyr's wiki.
(→Конктенация) |
м (→inds: Индексы) |
||
| Строка 59: | Строка 59: | ||
inds: T^ω стрелочк с волнлй Nat-infset | inds: T^ω стрелочк с волнлй Nat-infset | ||
inds FL={1..len FL} | inds FL={1..len FL} | ||
| + | |||
| + | ==Задача== | ||
Задача: пр. функцию length, которя выч. длину списка | Задача: пр. функцию length, которя выч. длину списка | ||
'''value''' | '''value''' | ||
| Строка 67: | Строка 69: | ||
length2(l) ≡ card inds l | length2(l) ≡ card inds l | ||
| + | ==Case== | ||
Конструкция case: | Конструкция case: | ||
'''case''' ''cond'' '''of''' | '''case''' ''cond'' '''of''' | ||
Версия 06:14, 27 сентября 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
Как это исп. для работы со спискми (на том же примере):
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)}
Формальная спецификация и верификация программ
|
|
