为什么 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.

并对其进行透析：

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

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

第二个版本的问题可以通过以下方式找到-Woverspecs：

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

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

这两个问题也可以通过极其不寻常的情况来检测-Wspecdiffs：

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

也不鼓励使用-Woverspecs任何-Wspecdiffs操作模式，因为 Dialyzer 的类型分析可以并且将会概括类型，因此“以更严格的方式指定的内容”可能是概括的结果。

也可能是您希望仅使用 0 和 1 作为参数来调用这些函数，在这种情况下规范为“ok”。