Immutable class in Eiffel

Question

I'm trying to make an immutable POINT class in Eiffel. Is the code below defines one? The {NONE} accessibility for the x and y fields is enough for it? Can I write something to the class invariant like x = x', or how else can I achieve immutability?

class POINT
    create
        make
    feature {NONE}
        x: DOUBLE
        y: DOUBLE
    feature
        make (x_: DOUBLE; y_: DOUBLE)
        do
            x := x_
            y := y_
        ensure
            set: x = x_ and y = y_
        end

    feature --accessors
        get_x: DOUBLE
        do
            Result := x
        ensure
            Result = x
        end
    end

Answer 1

Eiffel does not allow to change attributes of a class by its clients. For example, the following code is rejected:

p: POINT
...
p.x := 5.0

As a result, there is no need to provide getters (like in some other languages). You can just use p.x provided that x is sufficiently exported to a client class. So, the code of your example can be simplified to

class POINT
create
   make
feature -- Access
   x: DOUBLE
   y: DOUBLE
feature {NONE} -- Creation
   make (x0: DOUBLE; y0: DOUBLE)
      -- Initialize object with `x0' and `y0'.
   do
      x := x0
      y := y0
   ensure
      set: x = x0 and y = y0
   end
end

Note that the creation procedure is not exported anymore, otherwise it would be possible to use it as a normal (i.e. non-creation) routine and to change the attributes, that is we would be able to do something as follows

create p.make (1, 1)
p.make (2, 3)
print (p)

and this would print (2, 3), i.e. you would be able to change the value of the original object p, making it mutable.

Though, now the attributes cannot be changed directly, it's still possible to call feature copy on an object of type POINT and to change the whole object. If you want to avoid this situation as well, the feature can be redefined in the class POINT to raise an exception, or even to have a postcondition False causing the run-time to raise an exception for you:

copy (other: like Current)
      -- <Precursor>
   do
      (create {EXCEPTIONS}).raise ("Attempt to change an immutable object.")
   ensure then
      is_allowed: False
   end