none
What ForAll statements can be proven? Simple examples are not working!

    General discussion

  • I am surprised that simple examples like this cannot be proven.

    using System;
    using System.Collections.Generic;
    using System.Diagnostics.Contracts;
    using System.Linq;
    using System.Text;
    using System.Threading.Tasks;
    
    namespace TestCodeContracts
    {
      class Program
      {
        static void Main(string[] args)
        {
          var x = new int[] { 2, 4, 6 };
          if (Even(x))
          {
            Contract.Assert(Contract.ForAll(x, n => n % 2 == 0));
          }
        }
    
        static bool Even(int[] numbers)
        {
          Contract.Requires(numbers != null);
          Contract.Ensures(!Contract.Result<bool>() || Contract.ForAll(numbers, n => n % 2 == 0));
          return numbers.Aggregate(true, (acc, n) => acc && n % 2 == 0);
        }
    
      }
    
    }

    What ForAll statements can be proven? I have not found any examples myself.

    Here is another, even simpler, program it cannot prove.

    using System;
    using System.Collections.Generic;
    using System.Diagnostics.Contracts;
    using System.Linq;
    using System.Text;
    using System.Threading.Tasks;
    
    namespace TestCodeContracts
    {
      class Program
      {
        static void Main(string[] args)
        {
          Test(new int[] { });
        }
    
        static IEnumerable<int> Test(IEnumerable<int> xs)
        {
          Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<int>>(), x => true));
          return xs;
        }
    
      }
    
    }


    • Edited by erisco Saturday, April 09, 2016 7:49 PM
    Saturday, April 09, 2016 6:26 PM

All replies

  • I just read that the static checker does not support ForAll and Exists. This is highly disappointing. I am not sure what use I can get out of Code Contracts then.
    Saturday, April 09, 2016 8:00 PM