immutability - Eiffel の不変クラス

Question

私はPOINTエッフェルで不変のクラスを作ろうとしています。以下のコードはそれを定義していますか? とフィールドの{NONE}アクセシビリティは十分ですか? のようなクラス不変式に何かを書くことはできますか、または他にどのように不変性を達成できますか?xyx = x'

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