与艾菲尔的关键字“like`不变的分享

Question

在艾菲尔，可以指定一个'anchored declaration'的类型。

不知班上相关不变，亦适用于锚声明：

class C 

feature 

    f: INTEGER 
     do 
      ... Do something ... 
     end 

    g: like f 
     do 
      ... Do some other thing ... 
     end 

invariant 
    0 < f 
    -- 0 < g <-- Does this pop into existence? 
end 

我没有看到这在任何地方写的，我觉得它的情况并非如此。有时候避免定义另一种类型会很方便，但我认为这会限制所有其他情况下的锚定声明的用处。

Answer 1

不，不可能从锚定声明自动创建不变量。在该行中：

g: like f 

锚点类型“like f”只替换了“g”的类型。这与将“f”类型复制并粘贴为“g”类型非常相似。换句话说，在你的例子中，你写的东西几乎和直接写：

g: INTEGER