erlang - 为什么 Dialyzer 相信具有过于具体的返回类型的规范？

Question

我希望添加规范永远不会降低安全性，但这正是以下情况发生的情况。
在下面的代码中， Dialyzer (错误地)相信我 bar 的返回类型是 1 。这导致它说 foo() 中的模式永远不能匹配 - 如果注意不正确的建议，将引入运行时错误!

-module(sample).
-export([foo/0]).

foo() ->
    case bar() of
        1 -> ok;
        2 -> something
    end.

 -spec bar() -> 1.
bar() ->
  rand:uniform(2).

删除 bar/0 的规范可以解决问题——但为什么 Dialyzer 信任我？
Dialyzer 在这里违反了它的“无误报” promise :它在没有错误时发出警告。并且(甚至更糟)透析器轻推引入一个新的错误。

Answer 1

Dialyzer 在检查其规范之前计算每个函数的成功类型，此操作有几种可能的结果:

规范类型与成功类型不匹配:无效类型规范警告

规范类型是成功类型的严格父类(super class)型:警告仅使用 -Wunderspecs 或 -Wspecdiffs

规范类型是成功类型的严格子类型:仅对 -Woverspecs 或 -Wspecdiffs 发出警告。

规范类型和成功类型完全匹配:一切都很好

规范类型和成功类型重叠但不完全匹配(如 -1..1 和 pos_integer() ):同 2.

对于 1，它继续成功类型，否则继续成功类型和规范类型之间的交集。
您的情况是 3，通常不会被警告，因为作为程序员，您更了解(就透析器而言，也许 rand:uniform(2) 只能返回 1 )。你可以用

{dialyzer, [{warnings, [underspecs,overspecs]}]}.

在 rebar.config 文件中