@type 'a list 

@function nil: 'a list
@function cons: 'a, 'a list -> 'a list

@function first: 'a list -> 'a
@function rest: 'a list -> 'a list

@function length: 'a list -> int

@axiom L1: length(nil) = 0
@axiom L2: all lst: 'a list. 
		not(lst=nil) ==> 
		     length(lst) = 1 + length(rest(lst))

@requires true
@ensures len = length(lst)

@program 
	  @var len : int
          @var lst, temp : int list

	  temp = lst;
	  len = 0;

          @invariant len == length(lst) - length(temp)
	  while (temp != nil) {
		len = len + 1;
		temp = rest(temp);
	  }
@end
--