E.2.11 Bounded_Nat_List

spec

Bounded_List [Elem] [op bound : Nat] given Nat =

 

List [Elem] and Ordered_Nat

then

 

op

length : List[Elem] -> nat

vars

e:Elem; l:List[Elem]

axioms

 
length(nil) = zero;
length(cons(e,l)) = succ length(l)

sort

Bounded_List[Elem] = { l:List[Elem] · length(l) < bound }

type

Bounded_List[Elem] ::= nil | cons(

first:?Elem;

rest:?Bounded_List[Elem])?

%% The properties of the operations on Bounded_List[Elem] are
%% determined by their overloadings on List[Elem]

end

spec

Bounded_Nat_List [op bound : Nat] =
Bounded_List [view Nat_as_Elem] [op bound : Nat]