0

I'm new to Code Contract, and the document says all members that are mentioned in preconditions must be at least as accessible as the method itself, a private field cannot be mentioned in a precondition for a public method, therefore the code below doesn't compile:

using System;
using System.Diagnostics.Contracts;

public class UseFulLibrary{
   private static Item item = null;

   public static void Foo(Item newItem) {
      Contract.Requires(newItem != item);   // doesn't compile
   }
}
public class Item { }

But it is OK to access private member in a public method if we have:

public class UseFulLibrary{
   private static Item item = null;

   public static void Foo(Item newItem) {
      if (newItem != item) {
         ...
      }
   }
}

Clients can certainly call UseFulLibrary.Foo method, even though the client cannot access the private static Item field explicitly on their end, so why preconditions requires this unnecessary condition?

  • 4
    Code Contracts are [anandoned](https://stackoverflow.com/questions/64985444/are-code-contracts-supported-in-net-core). While the namespace is there and the code compiles, there's no rewriter so there's no way to enforce them. The contract code you write compiles to nothing. The only discussion is [whether to completely remove those classes or mark them as obsolete](https://github.com/dotnet/runtime/issues/23869) – Panagiotis Kanavos Apr 05 '21 at 07:16
  • 2
    In any case, what you try to do here can't be done with a code contract. `item` is writable so any method in `UseFullLibrary` can modify it. There's no way to check *at compile time* that `newItem` and `item` are different. Code contracts make little sense if they can't be evaluated at compile time. They'd be no different than `if (...) throw new ArgumentException()`. In fact, your second snipped behaves very differently from the first - it ignores duplicates instead of throwing – Panagiotis Kanavos Apr 05 '21 at 07:22
  • 1
    In any case, it's safer(and probably easier) to change the code so invalid operation won't compile. Eg, create the singleton instance in the static library itself instead of accepting one from the outside. Make the field `readonly`. Or use a proper singleton implementatiion - a public static property in *one* class visible by all others that's initialized either statically or through a `Lazy<>`. – Panagiotis Kanavos Apr 05 '21 at 07:26
  • 1
    Code contracts aside, suppose you are the caller of `Foo`, and sees that it has the precondition of "`newItem != item`", how can you ensure that you don't pass in something that violates the precondition, when the value of `item` is hidden from you!? – Sweeper Apr 05 '21 at 07:27
  • The functional techniques that started appearing in C# (pattern matching, switch expressions, records) allow you to write code that won't even allow "bad" cases. With a record, you ensure fields can't change after initialization. With switch expressions you can ensure no unexpected values are allowed (only up to a point unfortunately). Nullable types can ensure no `null`s can sneak unless explicitly allowed – Panagiotis Kanavos Apr 05 '21 at 07:30
  • @Sweeper sorry I don't get what you mean. Firstly, how does a caller know the library method s/he calls contains precondition? Secondly, the caller can pass whatever s/he wants, if the passed argument doesn't meet requirement, Contract will throw an exception, that's how Contract validation works, why limit user input? –  Apr 05 '21 at 09:11

0 Answers0