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

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

Перейти к: навигация, поиск

Содержание

Списки

Списки в 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
  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) → {(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

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


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

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