gmane.comp.lang.erlang.general

Paul Guyot | 18 Aug 09:51

Dialyzer confused by several clauses?

Hello,

Updating some code, I realized that dialyzer did not complain about  
an incorrect specification.

Here is a simple code that it accepts:

-type(dict() :: any()).

-spec(clause/2::(integer(), dict()) -> tuple()).
clause(0, Dict) ->
     case orddict:find(0, Dict) of
         {ok, Value} -> Value;
         error -> 0.0
     end;
clause(Integer, Dict) ->
     case orddict:find(Integer, Dict) of
         {ok, Value} -> Value / Integer;
         error -> 0.0
     end.

The real contract is:
-spec(clause/2::(integer(), dict()) -> float()).

An implied contact would be:
-spec(clause/2::(integer(), dict()) -> float() | any()).

But this contract is certainly incompatible with the code:
-spec(clause/2::(integer(), dict()) -> tuple()).

(Continue reading)

headers

Tobias Lindahl | 18 Aug 10:44

Re: Dialyzer confused by several clauses?

Paul,

Paul Guyot wrote:
> Hello,
> 
> Updating some code, I realized that dialyzer did not complain about an 
> incorrect specification.
> 
> Here is a simple code that it accepts:
> 
> -type(dict() :: any()).
> 
> -spec(clause/2::(integer(), dict()) -> tuple()).
> clause(0, Dict) ->
>     case orddict:find(0, Dict) of
>         {ok, Value} -> Value;
>         error -> 0.0
>     end;
> clause(Integer, Dict) ->
>     case orddict:find(Integer, Dict) of
>         {ok, Value} -> Value / Integer;
>         error -> 0.0
>     end.
> 
> The real contract is:
> -spec(clause/2::(integer(), dict()) -> float()).
> 
> An implied contact would be:
> -spec(clause/2::(integer(), dict()) -> float() | any()).
>

(Continue reading)

headers

Paul Guyot | 19 Aug 11:32

Re: Dialyzer confused by several clauses?

Le 18 août 08 à 10:44, Tobias Lindahl a écrit :

> The checking in Dialyzer whether a contract is valid is not as  
> sophisticated as it could be. First it finds the success typing of  
> a function and then it compares it with the contract. The default  
> is to complain only if the two are contradicting.
>
> In your case the return type in the success typing is any() because  
> of the Value in the first clause (*). Since this does not  
> contradict the tuple() in the contract, Dialyzer is satisfied. The  
> reason for this somewhat liberal reasoning is the principle of  
> sound warnings; if there is a possibility that a contract is  
> correct then Dialyzer gives no warning. However, we could of course  
> lift this restriction by allowing the user to give some option, but  
> this is not present today.
>
> There are options for getting more strict warnings about contracts.  
> However, they would not have helped you in this case. The options  
> are --Wunderspecs, --Woverspecs and --Wspecdiffs. Basically these  
> options makes Dialyzer warn when the specs differ from the success  
> typings of functions. They are not on by default since the  
> resulting warnings are a bit confusing at times.
>
> Tobias
>
> (*) As you say, the type could be written as float() | any(), but  
> unions must be disjoint so this is collapsed to any().

Dear Tobias,

(Continue reading)

headers

Tobias Lindahl | 19 Aug 12:35

Re: Dialyzer confused by several clauses?

Paul Guyot wrote:
> Le 18 août 08 à 10:44, Tobias Lindahl a écrit :
> Dear Tobias,
> 
> Thank you for your reply! And thanks for the hint about the options, 
> which actually detect the specification error.
> 
> I am somewhat confused by the type arithmetics used by dialyzer, 
> especially with unions. If code is of type any() | float() and 
> specification is of type tuple(), how can it match? In which case would 
> it be correct to match code[any() | x()] with spec[y()]?

Perhaps I was a bit unclear about the union type. The type float() | 
any() is not a valid union. The separate parts of the union must be 
disjoint, and since float() is a subtype of any() the union is collapsed 
to any().

Valid unions are for example tuple()|integer(), or 'ok'|{'error',any()}. 
Invalid unions would be something like byte()|integer(), 'ok'|atom(). Of 
course, there is nothing wrong with forming these unions, but they will 
be collapsed to integer() and atom() respectively.

When you specify that your function should return tuple(), and dialyzer 
finds that the function can return any() (because of the collapsed 
union), dialyzer simply assumes that you know better and accepts the 
annotation. Note that any() do not contradict tuple(), since tuple() is 
included in any().

Hope this made things a bit more clear.

(Continue reading)