为什么Dialyzer不能捕捉到这个简单的错误？

Question

透析器没有信号不一致在这个函数

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

的返回类型，但它在最后一行是

myfun(_) -> other_number. 

的情况下检测为什么会这样呢？ 以上应该是一个非常简单的例子，我相信......

感谢

Answer 1

最简单的答案类型的“透析为什么不......”是“，因为它已被设计成疑问总是正确的“或”因为它永远不会承诺它会抓住一切或任何特定的东西“。

---

对于更复杂的答案，您需要进一步指定您的问题。如果我写你的例子在一个模块中：

-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模式被鼓励，因为透析器的类型的分析能够而且将会概括的类型，所以“东西在被指定更具限制性的方式“可能是泛化的结果。

也可能出现这种情况，您打算只用0和1作为参数调用这些函数，在这种情况下，规范是“好的”。