class  counter  export  inc val  feature 
   count : Integer
   create  is do  count := 0  end 
   inc( n : Integer )  is 
  	 require  n > 0  do 
  	count := count + n
  	 ensure  count =  old  count + n
  	 end 
   val : Integer  is do   Result  := count  end 
    invariant  count >= 0
    end  -- class counter