45 lines
1.6 KiB
Markdown
45 lines
1.6 KiB
Markdown
List is the most fundamental data type. Is a sequencial argument, is a final sequence of element. It is no possible to have more than one element per box.
|
||
There is two different way to declare a list, the recursive one and the iterative one.
|
||
|
||
## Recursive list
|
||
- The first box is the **head of the list**
|
||
- The rest of the list is **the tail of the list**
|
||
- The signature of the recursive list is the following:
|
||
```
|
||
TYPES
|
||
list, box
|
||
|
||
USES
|
||
element
|
||
|
||
OPERATIONS
|
||
emptylist : -> list (* Internal operations of list*)
|
||
cons : element x list -> list (* Internal operations of list *)
|
||
tail : list -> list (* Internal operations of list *)
|
||
head : list -> box (* Internal operations of box *)
|
||
contents : box -> element (* Observer of box *)
|
||
first : list -> element (* Observer of list *)
|
||
next : box -> box (* Internal operation of box *)
|
||
|
||
PRECONDITIONS
|
||
tail(l) is-defined-iaoi l ≠ emptylist
|
||
head(l) is-defined-iaoi l ≠ emptylist
|
||
first(l) is-defined-iaoi l ≠ emptylist
|
||
|
||
AXIOMS
|
||
first(_l_) = contents(head(l))
|
||
tail(cons(_e,l_)) = l
|
||
first(cons(_e,l_)) = e
|
||
next(head(_l_)) = head(tail(l))
|
||
|
||
WITH
|
||
list l
|
||
element e
|
||
```
|
||
`cons` add en element to the head of the list (eg. li <- cons(cloud, li))
|
||
`head`return the element in the head of the list (eg. pl <- head(li))
|
||
`contents`return what is the element of the head
|
||
`first`return the first element of the list (is equivalent to contents)
|
||
`tail`remove the first element of the list (eg. fl <- tail (li))
|
||
`next`return the element after a box (eg. pspt <= next(head(li))))
|