erlang 为什么Dialyzer相信返回类型过于具体的规格?

unftdfkk  于 2022-12-08  发布在  Erlang
关注(0)|答案(2)|浏览(138)

我希望添加规范永远不会使事情变得 * 不 * 安全,但这正是在下面的情况下发生的。
在下面的代码中,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在这里违反了它的“无误报”承诺:当没有bug时,它会发出警告。而且(更糟糕的是)透析器会轻推引入一个新的bug。

fcwjkofz

fcwjkofz1#

Dialyzer calculates the success typing for each function before checking its spec, this action has several possible outcomes:

  1. The spec type does not match the success type: Invalid type spec warning
  2. The spec type is a strict supertype of the success type: Warning only with -Wunderspecs or -Wspecdiffs
  3. The spec type is a strict subtype of the success type: Warning only with -Woverspecs or -Wspecdiffs .
  4. The spec type and the success type match exactly: Everything's good
  5. The spec type and the success type overlap but don't match exactly (like -1..1 and pos_integer() ): Same as 2.
    For 1, it continues with the success type, otherwise continues with the intersection between the success type and the spec type.
    Your case is 3, which is usually not warned about because you, as the programmer, know better (as far as dialyzer is concerned, maybe rand:uniform(2) can only return 1 ). You can activate it with
{dialyzer, [{warnings, [underspecs,overspecs]}]}.

in the rebar.config file

ac1kyiln

ac1kyiln2#

透析器自身的分析(目前)是基于几种过度近似,因此它无法辨别您的更严格规范是由于您肯定是错误的还是由于透析器在某些地方过度近似。
因此,它选择信任您的规范,并在以后根据该信息报告明确的错误。
一般来说,其他现代系统的类型错误相关信息都是“报告所有部分,没有明确指定责任”。这里实际上是推理、规范和模式不兼容的情况,但Dialyzer只责怪模式。这是使用它时要记住的一个怪癖。

相关问题