为什么Dialyzer没有发现这个简单的错误

Question

Dialyzer不表示此函数的返回类型不一致：

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

但是它在最后一行是的情况下进行检测

myfun(_) -> other_number.

为什么会这样？我认为以上应该是一个非常简单的案例。

感谢

Answer 1

对于"为什么Dialyzer不…"类型的问题，简单的答案是"因为它被设计成总是正确的"或"因为它从不承诺会捕捉到所有或任何特定的东西"。

---

对于更复杂的答案，您需要进一步详细说明您的问题。如果我把你的例子写在一个模块里：

-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.

并对其进行透析：

$ 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)

这两个差异都没有被"检测到"，因为这两个都不是"错误"。只是在某些方面，代码比规范更通用（可以返回额外的值），在某些方面更具限制性（对于版本1，不能处理每个整数）。

第二个版本的问题可以用-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)

该警告准确地解释了规范比代码更具限制性。

这两个问题也可以通过极不寻常的-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)

-Woverspecs和-Wspecdiffs操作模式都不受鼓励，因为Dialyzer的类型分析可以并且将推广类型，所以"以更严格的方式指定的东西"可以是推广的结果。

也可能是这样的情况，即只使用0和1作为参数来调用这些函数，在这种情况下，规范是"ok"。