erlang 为什么透析器不能捕获这个简单的错误?

hs1rzwqc  于 2022-12-08  发布在  Erlang
关注(0)|答案(1)|浏览(124)

透析器未发出该函数返回类型不一致的信号:

-spec myfun(integer()) -> zero | one.
myfun(0) -> zero;
myfun(1) -> one;
myfun(2) -> other_number.

但是在最后一行

myfun(_) -> other_number.

为甚么会这样呢?我相信以上应该是一个很简单的例子。
谢谢

tyu7yeag

tyu7yeag1#

The easy answer to questions of type "why Dialyzer doesn't..." is "because it has been designed to be always correct" or "because it never promises that it will catch everything or anything specific".
For the more complex answer, you need to specify your question further. If I write your example in a module:

-module(bar).

-export([myfun1/1, myfun2/1]).

-spec myfun1(integer()) -> zero | one.

myfun1(0) -> zero;
myfun1(1) -> one;
myfun1(2) -> other_number.

-spec myfun2(integer()) -> zero | one.

myfun2(0) -> zero;
myfun2(1) -> one;
myfun2(_) -> other_number.

And Dialyze it:

$ dialyzer bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.64s
done (passed successfully)

... neither discrepancy is 'detected', cause neither is an "error". It's just the case that the code is in some ways more generic (can return extra values) and in some ways more restrictive (cannot handle every integer, for version 1) than the spec.
The second version's problem can be found with -Woverspecs :

$ dialyzer -Woverspecs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.58s
done (warnings were emitted)

The warning explains exactly that the spec is more restrictive than the code.
Both problems can also be detected by the extremely unusual -Wspecdiffs :

$ dialyzer -Wspecdiffs bar.erl 
  Checking whether the PLT /home/stavros/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis...
bar.erl:5: Type specification bar:myfun1(integer()) -> 'zero' | 'one' is not equal to the success typing: bar:myfun1(0 | 1 | 2) -> 'one' | 'other_number' | 'zero'
bar.erl:11: Type specification bar:myfun2(integer()) -> 'zero' | 'one' is a subtype of the success typing: bar:myfun2(_) -> 'one' | 'other_number' | 'zero'
 done in 0m0.61s
done (warnings were emitted)

Neither -Woverspecs nor -Wspecdiffs mode of operation is encouraged, as Dialyzer's type analysis can and will generalize types, so "something being specified in a more restrictive way" can be the result of generalization.
It can also be the case that you intend these functions to be called only with 0 and 1 as arguments, in which case the spec is 'ok'.

相关问题