epicours/Algo/CM/Lists.md

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 : list x element -> 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_