multidimensional arrays as Return types, Access permissions

[alex28sh]

Hello, I have currently some issues with proving access permissions for the elements of bidimensional array, when returning it. For example Ensures(Forall(Result(), lambda d_0_s_: Acc(list_pred(d_0_s_)))) doesn't work, while Requires(Forall(strings, lambda d_0_s_: Acc(list_pred(d_0_s_)))) for the input parameter works well.

I wonder if there is any way to get around this problem. Thank you for considering this request.

Below you can find the example of function declaration, that I'm trying to verify:

def filter__by__substring(strings : List[List[int]], substring : List[int]) -> List[List[int]]:
    Requires(Acc(list_pred(strings)))
    Requires(Forall(strings, lambda d_0_s_: Acc(list_pred(d_0_s_))))
    Requires(Acc(list_pred(substring)))
    Ensures(Acc(list_pred(strings)))
    Ensures(Forall(strings, lambda d_0_s_: Acc(list_pred(d_0_s_))))
    Ensures(Acc(list_pred(Result())))
    Ensures(Forall(Result(), lambda d_0_s_: Acc(list_pred(d_0_s_)))) <- Type error: Encountered Any type. Type annotation missing
    Ensures((len(Result())) <= (len(strings)))

Best regards, Alex

[marcoeilers]

Once PR #205 is merged, you can write ResultT(List[List[int]]) instead.