immutability - Eiffel 的一成不变

我正在尝试在Eiffel中创建一个不变的POINT类。下面的代码定义一个吗？ {NONE}和x字段的y可访问性就足够了吗？我可以像x = 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

最佳答案

Eiffel不允许其客户更改类的属性。例如，以下代码被拒绝:

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

结果，不需要提供 setter/getter (就像其他语言一样)。您可以只使用p.x，前提是x已充分导出到客户端类。因此，您的示例代码可以简化为

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

请注意，创建过程不再是而不是导出，否则可以将其用作常规(即非创建)例程并更改属性，也就是说，我们可以执行以下操作

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

这将打印(2, 3)，即您将能够更改原始对象p的值，使其可变。

尽管现在不能直接更改属性，但仍然可以在copy类型的对象上调用功能POINT并更改整个对象。如果还想避免这种情况，则可以在类POINT中重新定义该功能以引发异常，甚至可以使后置条件False导致运行时为您引发异常:

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

关于immutability - Eiffel 的一成不变，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/20938164/