Class invariant to ensure a particular data type on a field does not hold

Question

Given the following code:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;

using System;

public class Program
{
    public int[] ints = new int[1000];

  [ContractInvariantMethod]
  private void ObjectInvariant ()
  {
    Contract.Invariant(ints.GetType() == typeof(int[]));
    Contract.Invariant(ints != null);
  }
}

Why is the invariant ints.GetType() == typeof(int[]) considered to cannot be proven? If I change the invariant to ints.GetType() == ints.GetType() it passes (without any surpise), but why does it fail for typeof(int[]).

score 2 · Accepted Answer · answered Dec 20 '18 at 16:02

2

Sadly, you can in fact store objects in an int[] that aren't actually an int[]. There are some valid conversions that you would hope wouldn't be valid, but that in fact are. For example, someone could write:

ints = (int[])(object)new uint[5];

and now the type of ints is an unsigned int array, not an int array. That this conversion is valid is unfortunate (that it's valid almost exclusively just causes bugs when it comes up); it's be great if what you posted could be an invariant, but sadly, Contract.Invariant is correct that it's not.

answered Dec 20 '18 at 16:02

Servy

202,030
26
332
449

1

I couldn't believe this first, but you are right. Is this crazy language (or CLR?) feature somewhere documented? – Klaus Gütter Dec 20 '18 at 16:13
Then what's the right way to check that elemnts of `ints` are actually of type `int`? – cristid9 Dec 20 '18 at 16:16
@KlausGütter Off hand, I believe that the conversion is invalid in the C# type system (hence why it won't compile without the cast to `object`), but valid in the CLR, so the compiler will try to prevent the conversion but the CLR will allow it. – Servy Dec 20 '18 at 16:16
Thank you. In the meanwhile I found https://stackoverflow.com/questions/593730/why-does-int-is-uint-true-in-c-sharp where Jon's answer confirms what you say. – Klaus Gütter Dec 20 '18 at 16:18
1

@cristid9 um...you wrote the code to check it. It just has to be a runtime check, not a compile time check. Now you can get an item from the array and treat it as an `int`. It might not behave the way you want (you'd be treating an unsigned int's bits as if it were a signed int, giving you a messed up value) but you can do it. – Servy Dec 20 '18 at 16:18
@KlausGütter Of course you probably don't *want* to go around checking for this whenever you've got an int array. You probably just want to assume the int array is an int array, and if someone does something evil like this you just blame them for using your type in an inappropriate way. Garbage in garbage out and all that. – Servy Dec 20 '18 at 16:22
Got it working with this one `Contract.Invariant(ints[0] is int);` – cristid9 Dec 20 '18 at 16:33
And interestingly `ints[0].GetType()` is typeof(int) even if `ints.GetType()` is typeof(uint[]). – Klaus Gütter Dec 20 '18 at 16:34
@cristid9 In that case the code has already converted the `uint` to an `int` when it was returned by the indexer (it just has a mangled value by that point). Also, what if the array is empty? – Servy Dec 20 '18 at 16:35
Man, it is a homework, all they ask me is to write an invariant to "Write the object (class) invariants that ensure that arrays represent sets of Integers." So I think all I need to do is to check if `ints` contains ints and there are no duplicates in the array. – cristid9 Dec 20 '18 at 16:36
1

@cristid9 Sure sounds like a really poorly designed assignment to me (unless there's more to it than you've described). Probably worth bringing up with your instructor. – Servy Dec 20 '18 at 16:38

Class invariant to ensure a particular data type on a field does not hold

1 Answers1