Static checker has difficulty proving assertions when booleans are involved

Question

I have this function:

internal static bool IsNullableValue(this Type type)
{
    Contract.Requires(type != null);
    return type.IsGenericType && !type.IsGenericTypeDefinition && type.GetGenericTypeDefinition() == typeof(Nullable<>);
}

I would like to add the following postcondition:

 

 

Contract.Ensures(!Contract.Result<bool>() || type.GetGenericArguments().Length > 0);

In an ideal world, Type methods would have sufficient postconditions, and I would not have to make assumptions. However, that's not my point.

I add an assumption:

 

 

internal static bool IsNullableValue(this Type type)
{
    Contract.Requires(type != null);

    Contract.Ensures(!Contract.Result<bool>() || type.GetGenericArguments().Length > 0);

    bool result = type.IsGenericType && !type.IsGenericTypeDefinition && type.GetGenericTypeDefinition() == typeof(Nullable<>);

    Contract.Assume(!result || type.GetGenericArguments().Length > 0);

    return result;
}

The static checker is not able to prove the postcondition!

When I change the code as follows:

 

 

internal static bool IsNullableValue(this Type type)
{
    Contract.Requires(type != null);

    Contract.Ensures(!Contract.Result<bool>() || type.GetGenericArguments().Length > 0);

    bool result = type.IsGenericType && !type.IsGenericTypeDefinition && type.GetGenericTypeDefinition() == typeof(Nullable<>);

    if (result)
    {
        Contract.Assume(type.GetGenericArguments().Length > 0);
        return result;
    }
    else
    {
        return result;
    }
}

Now the postcondition is proven.

However, I do not want to write code that says if (boolean) return true; else return false;
Or even worse, if (result) return result; else return result;

I believe this is a limitation of the static checker that I would call a bug, and that needs fixing.

I'm using code contract V1.2.21023.14 on Visual Studio 2010 beta 2.


Thanks,

Kris.

 

 

Answer 1

Thanks for reporting this. It's pointing to a precision problem in the static checker in that we fail to materialize the value of the pure function GetTypeArguments() in the disjunction, which causes the checker to think that the second call to it might give a different value.

The current workaround would be to force materialization of the pure function value in the static checker by having some call to GetTypeArguments() that is not conditional. E.g., if you add the silly 

 

 

Contract.Assume(type.GetGenericArguments() != null || type.GetGenericArguments() == null);

or simply

  var dummy = type.GetGenericArguments();

in the method body, it passes.

(well maybe you need the missing Pure assumption on GetGenericTypeDefinition() as well that I added when i saw your example).


I now added a bunch extra contracts on mscorlib on types. Now the following passes on my internal build:

  internal static bool IsNullableValue(this Type type)
  {
    Contract.Requires(type != null);
    Contract.Ensures(!Contract.Result<bool>() || type.GetGenericArguments().Length > 0);


    var dummy = type.GetGenericArguments();


    bool result = type.IsGenericType && !type.IsGenericTypeDefinition && type.GetGenericTypeDefinition() == typeof(Nullable<>);

    return result;
  }

I'll have to do some work to make the "dummy" reference GetGenericArguments unnecesary.

Thanks again for pointing this out.

---

Cheers, -MaF (Manuel Fahndrich)