Erlang Dialyzer整数範囲

Question

-module(test). 
-export([f/0, g/0]). 

-spec f() -> RESULT when 
     RESULT :: 0..12 . 

-spec g() -> RESULT when 
     RESULT :: 0..13 . 

f() -> 100 . 

g() -> 100 . 

実行中の透析装置（およびタイパー）は、機能fのみが捕捉されます。

dialyzer test.erl 
Checking whether the PLT /Users/ben/.dialyzer_plt is up-to-date... yes 
Proceeding with analysis... 
test.erl:4: Invalid type specification for function test:f/0. The success typing is() -> 100 
done in 0m0.53s 
done (warnings were emitted) 

タイパー

typer test.erl 
typer: Error in contract of function test:f/0 
     The contract is:() -> RESULT when RESULT :: 0..12 
     but the inferred signature is:() -> 100 

と同じことが、この "期待される" 行動ですか？

Answer 1

はい、「期待されている」ようです。 ソースコードhere を見てみるとそれはテスト

t_from_range(X, Y) when is_integer(X), is_integer(Y) -> 
    case ((Y - X) < ?SET_LIMIT) of 
    true -> t_integers(lists:seq(X, Y)); 
    false -> 
     case X >= 0 of 
    false -> 
     if Y < 0 -> ?integer_neg; 
     true -> t_integer() 
     end; 
    true -> 
     if Y =< ?MAX_BYTE, X >= 1 -> ?int_range(1, ?MAX_BYTE); 
     Y =< ?MAX_BYTE -> t_byte(); 
     Y =< ?MAX_CHAR, X >= 1 -> ?int_range(1, ?MAX_CHAR); 
     Y =< ?MAX_CHAR -> t_char(); 
     X >= 1   -> ?integer_pos; 
     X >= 0   -> ?integer_non_neg 
     end 
     end 
    end; 

で

-define(SET_LIMIT, 13).

の値に対してテスト私見これは危険なようで、任意の実際の保証を提供していません。間違いなく明確に文書化されるべきです。 learn you some Erlangのウェブサイトに参照を渡しています。

整数の範囲です。たとえば、1年に月の数字 を表したければ、範囲1..12を定義できます。 Dialyzerは、この範囲をより大きなものに拡大する権利を留保しています。キーワードを使用して

しかし、何も公式のGoogleのフロントページにdialyzer integer ranges

編集...少し近いあなたがしようとすることを見ることができます探して：

-module(test). 
-export([h/0]). 

-spec h() -> RESULT when 
     RESULT :: 1..13 . 

h() -> 100 . 

ダイアライザーをキャッチしますエラー！ （Typerはしません）...

Answer 2

はい、「期待される」動作です。あるいはむしろ「受け入れられる」。

免責事項：すべてのエラーをキャッチすることを約束したことはありません

1. ダイアライザー。
2. 上記のコードはかなり人工的です。

---

説明：

透析装置の設計者は、再帰関数を解析する際（不動点に達する）ツールの型推論分析が終了します（他の理由の中）に、このようoverapproximations使用することを決定しました（内部階段は実際には次のようになります： "階乗の基底は0のために働きます。したがって、1のための再帰的な場合も働くので、2のためにも働くので、3の[...]でも働くので、 OKだから、char()でも動作しますが、char_range + 1でも動作しますので、すべて0123で動作します"）。

この（任意の実際に）制限が致命的になることは非常にまれで、Dialyzerは何も報告することを決して約束しませんでした...