Objects in Eiffel are defined by classes.
A typical class definition is given in slide
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 for a variable x of type counter.
The reserved word Result
is used to return a value from a function
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.