How can I use Code Contracts to ensure that a non-blank, non-null val should always be returned from a method?

Question

This code:

private static char GetBarcodeChecksumWithLegacyCode(string barcodeWithoutCzechSum)
{
    Contract.Requires(!string.IsNullOrWhiteSpace(barcodeWithoutCzechSum));
    Contract.Ensures(Contract.Result != null);
    . . .

...doesn't compile ("Operator '!=' cannot be applied to operands of type 'method group' and ''").

This fails the same way:

Contract.Ensures(Contract.ValueAtReturn != null);

How can I enforce the necessity of the method returning a result using Code Contracts?

UPDATE

If I do this:

Contract.Ensures(Contract.Result<char>() != '');

...it fails with, "Empty character literal"

So is this the way to test for the returned char val being both non-null and non-empty:

Contract.Ensures(Contract.Result<char>() != null && Contract.Result<char>().ToString() != string.Empty);

...or does the null check suffice?

BTW, trying to use ValueAtReturn instead of Result gives me "No overload for method 'ValueAtReturn' takes 0 arguments"

UPDATE 2

This code:

Contract.Ensures(Contract.Result<String>() != null && Contract.Result<String>() != string.Empty); 

fails with:

In method BarcodeCzechDigitTester.Form1.GetBarcodeChecksumWithLegacyCode(System.String): Detected a call to Result with 'System.String', should be 'System.Char'.

(twice) Also: "The command ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite.exe" "@BarcodeCzechDigitTesterccrewrite.rsp"" exited with code 2."

...but changing the code to this works:

Contract.Ensures(Contract.Result<char>() != null && Contract.Result<char>().ToString() != string.Empty);

Answer 1

You need to have it like:

Contract.Ensures(Contract.Result<string>() != null);

Answer 2

char is value type, it cannot be null.

char is not collection (like string or array), it cannot be empty.

If your method is returning bar code check-sum numeric character, then your contract can check for check-sum character values like this:

Contract.Ensures ( '0' <= Contract.Result<char>() && Contract.Result<char>() <= '9' );