3

free_vars_in_dterm({var, V}) -> {var, V};显然无法输入检查，但是，透析器说一切正常。

$ dialyzer *erl
  Checking whether the PLT ~/.dialyzer_plt is up-to-date... yes
  Proceeding with analysis... done in 0m0.66s
done (passed successfully)

代码如下：

-module(formulas).

-type formulas() :: {predicate(), [dterm()]}
                  | {'~', formulas()}
                  | {'&', formulas(), formulas()}
                  | {'|', formulas(), formulas()}
                  | {'->', formulas(), formulas()}
                  | {'<->', formulas(), formulas()}
                  | {'exist', variable(), formulas()}
                  | {'any', variable(), formulas()}.

-type dterm() :: constant()
               | variable()
               | {func(), [dterm()]}.

-type constant() :: {const, atom()}
                  | {const, integer()}.

-type variable() :: {var, atom()}.

-type func() :: {function,
                 Function_name::atom(),
                 Arity::integer()}.

-type predicate() :: {predicate,
                      Predicate_name::atom(),
                      Arity::integer()}.


-include_lib("eunit/include/eunit.hrl").

-export([is_ground/1, free_vars/1, is_sentence/1]).

-spec is_ground(formulas()) -> boolean().
is_ground({_, {var, _}, _}) -> false;
is_ground({{predicate, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms);
is_ground(Formulas) ->
    Ts = tuple_size(Formulas),
    lists:all(fun is_ground/1, [element(I, Formulas)
                                || I <- lists:seq(2, Ts)]).

-spec is_ground_term(dterm()) -> boolean().
is_ground_term({const, _}) -> true;
is_ground_term({var, _}) -> false;
is_ground_term({{function, _, _}, Terms}) ->
    lists:all(fun is_ground_term/1, Terms).


-spec is_sentence(formulas()) -> boolean().
is_sentence(Formulas) ->
    sets:size(free_vars(Formulas)) =:= 0.

-spec free_vars(formulas()) -> sets:set(variable()).
free_vars({{predicate, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]);
free_vars({_Qualify, {var, V}, Formulas}) ->
    sets:del_element({var, V}, free_vars(Formulas));
free_vars(Compound_formulas) ->
    Tp_size = tuple_size(Compound_formulas),
    join_sets([free_vars(element(I, Compound_formulas))
               || I <- lists:seq(2, Tp_size)]).

-spec free_vars_in_dterm(dterm()) -> sets:set(variable()).
free_vars_in_dterm({const, _}) -> sets:new();
free_vars_in_dterm({var, V}) -> {var, V};
free_vars_in_dterm({{function, _, _}, Dterms}) ->
    join_sets([free_vars_in_dterm(Dterm)
               || Dterm <- Dterms]).

-spec join_sets([sets:set(T)]) -> sets:set(T).
join_sets(Set_list) ->
    lists:foldl(fun (T, Acc) -> sets:union(T, Acc) end,
                sets:new(),
                Set_list).
4

1 回答 1

4

首先是一个简短的回答，使用 Dialyzer 的格言：

  1. 透析器永远不会出错。（经常被 Erlang 程序员背诵）
  2. Dialyzer 从未承诺会找出代码中的所有错误。（没那么出名）

Maxim 2 是对任何“为什么 Dialyzer 没有发现这个错误”问题的“标准”答案（诚然不是很令人满意）。

更多解释性答案：

Dialyzer 对函数返回值的分析经常过度近似。因此，类型中包含的任何值都应被视为“可能返回”的值。这有一个不幸的副作用，有时肯定会返回的值（例如您的{var, V}元组）也被认为是“可能返回”。Dialyzer 必须保证 maxim 1（永远不会出错），因此在“可能返回”意外值的情况下，它不会发出警告，除非没有任何实际指定的值可以返回。最后一部分在整个函数的级别进行检查，并且由于在您的示例中某些子句确实返回集，因此不会生成警告。

于 2017-03-29T06:47:57.173 回答