Свойства списков:
- каждый элемент может встретиться несколько раз
- порядок определен (и существенен)
type
LT1 = T1-list
NLT1 = T1-inflist
<.1,2,3.>
<..>
списочное выражение (rangered list expression)
<.3...7>═ =═ <.3,4,5,6,7.>
<.3..3.> = <.3.>
<.3..2.> = <..>
генерация списка на основе имеющегося
<. 2*n | n in <.1..100.> :- true .>
<. 2*n | n in <.1..100.> .>
<.n | n in <.1..100.> :- is_a_prime(n).> = ...
value
════ INTLIST : (Int >< Int)-list = <. (1,2), (2,2), (2,1), (3,1).>
.....
....... <. (x,f(y)) | (x,y) in INTLIST :- x>y .>
^ ══════════ :══ ════ T-list >< T-list -> T-list══════ concatenation
in ═════════ :══ ════ T >< T-list
len ═══════ :═ ═════ T-list -> Nat
hd ════════ :═ ═════ T-list -~-> T
tl ══════════ :═ ═════ T-list -~-> T-list
inds ════ :═ ═════ T-list -> Nat-set
elems ═ :═ ═════ T-list -> T-set
n Диаграмма Гогена
|
|
inds fl = {1..len fl}════════════════════════════ - для конечных списков
inds il = {idx | idx : Nat :- idx >= 1} - для бесконечных cписков
elems l = {l(idx) | idx : Nat :- idx isin inds l}
"abc"═ = <.'a','b','c'.>
"" = <..>
QUEUE =
═ class
═══ type
═════ Element,
═════ Queue = Element-list
═══ value
═════ empty : Queue,
═════ put : Element >< Queue -> Queue,
═════ get : Queue -~-> Queue >< Element
═══ axiom forall e : Element, q : Queue
═════ empty is <..>,
═════ put (e,q) is q ^ <.e.>,
═════ get(q) is (tl q, hd q)
═════ pre q ~= empty
end
(Объяснить, что forall √ это сокращенная запись, инструментом не поддерживается)
Следующий пример показывает, как строятся иерархии классов с расширениями (extend).
Вторая цель═ примера √ показать ⌠хороший стиль■. Здесь мы не будем описывать алгоритмы. Мы описываем только свойства результата.
LIST_PROPERTIES =
═ class
═══ value
═════ is_permutation : Int-list >< Int-list -> Bool,
═════ is_sorted : Int-list -> Bool
═══ axiom forall l,l1,l2 ; Int-list :-
═════ is_permutation(l1,l2) is
═══════ (all i : Int :-
══════════ card {idx | idx : Nat :- idx isin l1 /\ l1(idx) = i} =
══════════ card {idx | idx : Nat :- idx isin l2 /\ l2(idx) = i},
═════ is_sorted(l) is
═══════ (all idx1,idx2 : Nat :-
═════════ {idx1,idx2} <<= inds l /\ idx1 < idx2 =>
═══════ ════l(idx1) <= l(idx2))
end
Ниже приведено расширение рассмотренного выше модуля
SORTING =
═ extend LIST_PROPERTIES with
═ class
═══ value
═════ sort : Int-list -> Int-list
═══ axiom forall l : Int-list :-
═════ sort(l) as l1 post is_permutation(l1,l2) /\ is_sorted(l1)
end
Более сложный пример. Цель примера: сравнить впоследствие спецификации Database в термина сорт-типов, множеств кортежей и списков записей.
KEY =
═ class
═══ type
═════ Key
═══ value
═════ less_than : Key >< Key -> Bool
═══ axiom forall k,k1,k2,k3 : Key :-
═════ [anti_reflexive]
═══════ ~less_than(k,k),
═════ [transitive]
══════ ═less_than(k1,k2) /\ less_than(k2,k3) => less_than(k1,k3),
═════ [total_order]
═══════ less_than(k1,k2) \/ less_than(k2,k1) \/ k1=k2
end
DATA =
═ class
═══ type
═════ Data
═══ value
═════ not_found : Data
end
RECORD =
═ extend KEY with extend DATA with
═ class
═══ type
═════ Record = Key >< Data
═══ value
═════ new_record : Key >< Data -> Record,
═════ key_of : Record -> Key,
═════ data_of : Record -> Data
═══ axiom forall k : Key, d : Data :-
═════ new_record(k,d) is (k,d),
═════ key_of(k,d) is k,
═════ data_of(k,d) is d
end
LIST_DATABASE =
═ extend RECORD with
═ class
═══ type
═════ Database = {| rl : record-list :- is_wf_Database(rl) |}
═══ value
═════ is_wf_Database : Record-list -> Bool,
═════ empty : Database,
═════ insert : Key >< Data >< Database -> Database,
═════ remove : Key >< Database -> Database,
═════ defined : Key >< Database -> Bool,
═════ lookup : Key >< Database -> Data
═══ axiom forall k : Key, d : Data, rl : record-list db : Database :-
═════ is_wf_Database(rl) is
═══════ (all r1,r2 : Record, left,right : Record-list :-
═════════ rl = left ^ <.r1,r2.> ^ right =>
═══════════ less_than(key_of(r1),key_of(r2))),
══════ empty is <..>,
══════ insert(k,d,db) as db1
═════ ═post elems db1 = (elems remove(k,db)) union {new_record(k,d)},
══════ remove(k,db) is <.r | r in db :- key_of(r) ~= k.>,
══════ defined(k,db) is
════════ if db = <..> \/ less_than(k,key_of(hd db)) then false
════════ else key_of(hd db) = k \/ defined(k,tl db)
════════ end,
══════ lookup(k,db) is
═══════ ═if db = <..> \/ less_than(k,key_of(hd db)) then not_found
════════ elsif key_of(hd db) = k then data_of(hd db) then data_of(hd db)
════════ else lookup(k, tl db)
════════ end
end
n Свойства отображений:
- каждый ключ может встретиться только один раз
- порядок ключей не определен
type
MT12 = T1 -m-> T2
[1 +> true, 3+>false, 2+>true]
[]
[⌠Petrov■+>■912-5317■, ⌠Ivanov■+>■125-7652■
генерация отображения
[ n+>2*n | n : Nat :- n < 100 ]
dom
rng
m(k)══ - ⌠применение■ - найти значение по ключу k в отображении m
!!═ (├)═ - (dagger) добавить или переопределить значение ключа (override)
union═ - добавить (но не переопределить)
#═ (╟)══ - композиция
\ - убрать ключи из s
/ - оставить только ключи из s
m \ s = [d +> m(d) | d : T1 :- d isin dom m /\ d ~isin s] /* restricted by */m / s = [d +> m(d) | d : T1 :- d isin dom m /\ d isin s]═ /* restricted to */
n Диаграмма Гогена
|
|
Пример с использованием MAP
LIBRARY_MAP =
═ class
═══ type
══════ Books = Book-set,
══════ Log = Book -m-> Reader,
══════ Readers = Reader-set,
══════ Reader, Book
═══ value
═══════ book_out : Reader >< Readers >< Book >< Books>< Log-~-> Log
........book_in : Book >< Books >< Log -~-> Log,
═══════ register : Reader >< Readers -~-> Readers
═══════ register : Book >< Books -~-> Books
......
end