Свойства списков:
- каждый элемент может встретиться несколько раз
- порядок определен (и существенен)
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