It seems that NotNull and ContractAnnotation("key: null => halt") are fairly similar in their effect on R#. Is there something that I am missing? Should I always apply both?
They're very similar, but are semantically very different.
NotNull states that the target is expected to not be null, but makes no statements about the consequences. There might be a null check that throws an ArgumentNullException, or it might just use it without checking, and you could get a runtime NullReferenceException. Equally, the application might check for null, log it and continue safely.
ContractAnnotation("key: null => halt") tells ReSharper that if the key parameter is null, then the program flow terminates. ReSharper can use this like so:
string foo = null;
Assert.NotNull(foo); // ContractAnnotation("null => halt")
Assert.Equal(12, foo.length);
The second assert in this snippet will be marked as dead code, because ReSharper knows the first assert will throw when passed a null.
However, if Assert.NotNull was just marked with the NotNull attribute, then ReSharper would highlight the foo parameter with a warning, telling you that you shouldn't be passing a null value, but it doesn't know what will happen if you do.
Subtle, but different. I'd stick to the NotNull attribute if you require the value to never be null, and use ContractAnnotation("null => halt") for an assert style method that will definitely and explicitly throw if passed a null.