エッフェルのキーワード「好き」との不変の共有

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」のタイプのみを置き換えます。これは "g"のタイプとして "f"のタイプをコピーして貼り付けるのと非常によく似ています。言い換えれば、あなたの例では、あなたが書いたものは直接書くこととほぼ同じです：

g: INTEGER