Optional in cycles

[alex28sh]

Hello! Currently I'm having issues verifying code with Optional types. For example, for code containing cycles I get following error: Loop invariant issubtype(typeof(a), int()) might not hold on entry. (<no position>)

Here is the example of code:

    a = int(0) # type : Optional[int]
    a = None # type : Optional[int]
    d_4_i_ = int(0) # type : int
    while (d_4_i_) < (len(arr)):
        Invariant(Acc(list_pred(arr)))
        Invariant(((0) <= (d_4_i_)) and ((d_4_i_) <= (len(arr))))
        if (((arr)[d_4_i_]) < (0)) and (((a) is None) or (((arr)[d_4_i_]) >= (a))):
            a = ((arr)[d_4_i_])
        d_4_i_ = (d_4_i_) + (1)

Could you kindly help me with this problem?

[marcoeilers]

That looks like a Nagini bug to me. Could you send me the entire program you're verifying so I can try to reproduce it?

[alex28sh]

The whole version of program (but, for now, without any complicated invariants and postconditions) is like that:

from typing import cast, List, Dict, Set, Optional, Union, Tuple
from nagini_contracts.contracts import *

def largest__smallest__integers(arr : List[int]) -> Tuple[Optional[int], Optional[int]]:
    Requires(Acc(list_pred(arr)))
    Ensures(Acc(list_pred(arr)))
    a = int(0)
    b = int(0)
    a = None # type : Optional[int]
    b = None # type : Optional[int]
    d_4_i_ = int(0) # type : int
    d_4_i_ = 0
    while (d_4_i_) < (len(arr)):
        Invariant(Acc(list_pred(arr)))
        Invariant(((0) <= (d_4_i_)) and ((d_4_i_) <= (len(arr))))
        if (((arr)[d_4_i_]) < (0)) and (((a) is None) or (((arr)[d_4_i_]) >= (a))):
            a = ((arr)[d_4_i_])
        if (((arr)[d_4_i_]) > (0)) and (((b) is None) or (((arr)[d_4_i_]) <= (b))):
            b = ((arr)[d_4_i_])
        d_4_i_ = (d_4_i_) + (1)
    return (a, b)

[marcoeilers]

Hm, that's weird, Nagini seems to be getting incorrect type information about the type of a from Mypy. I'll try to figure out why, but as a workaround, you can use the other kind of type annotation for the first assignment to a, that seems to fix it:

    a: Optional[int] = int(0)  
    a = None

[alex28sh]

Thank you, that works!