Instructors' Guide

Introduction Terminology Expressions Control Objects Inheritance Technology Summary


Objects in Eiffel are defined by classes. A typical class definition is given in slide eiffel-objects. The class counter exports the features inc and val. The feature count is hence private to an instance of counter, since it does not appear in the interface defined by the export part.
    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
   val : Integer  is do   Result  := count  end 
    invariant  count >= 0
    end  -- class counter

slide: Eiffel -- objects

The create feature is automatically exported, and is used to create an instance of counter by the statement x.create for a variable x of type counter. The reserved word Result is used to return a value from a function feature. The method feature inc specifies both a pre-condition and a post-condition. The reserved word old is used to access the value of the instance variable count before evaluating inc. Finally, the invariance states the constraint that a counter instance never has a value below zero.