StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>Imagine you have a method like this:</p> <pre><code>bool ContainsAnX(string s) { return s.Contains("X"); } </code></pre> <p>Now, this method will always fail if you pass <code>null</code> to it, so you want to ensure this never happens. This is what <code>Contract.Requires</code> is for. It sets a <strong>precondition</strong> for the method, which must be true in order for the method to run correctly. In this case we would have:</p> <pre><code>bool ContainsAnX(string s) { Contract.Requires(s != null); return s.Contains("X"); } </code></pre> <p>(<strong>Note</strong>: <code>Requires</code> and <code>Ensures</code> must always be at the start of a method, as they are information about the method as a whole. <code>Assume</code> is used in the code itself, as it is information about that point in the code.)</p> <p>Now, in your code that calls the method "ContainsAnX", you must ensure that the string is not null. Your method might look like this:</p> <pre><code>void DoSomething() { var example = "hello world"; if (ContainsAnX(example)) Console.WriteLine("The string contains an 'X'."); else Console.WriteLine("The string does not contain an 'X'."); } </code></pre> <p>This will work fine, and the static checker can prove that <code>example</code> is not null.</p> <p>However, you might be calling into external libraries, which don't have any information about the values they return (i.e. they don't use Code Contracts). Let's change the example:</p> <pre><code>void DoSomething() { var example = OtherLibrary.FetchString(); if (ContainsAnX(example)) Console.WriteLine("The string contains an 'X'."); else Console.WriteLine("The string does not contain an 'X'."); } </code></pre> <p>If the <code>OtherLibrary</code> doesn't use Code Contracts, the static checker will complain that <code>example</code> might be null.</p> <p>Maybe their documentation for the library says that the method will never return null (or <em>should</em> never!). In this case, we know more than the static checker does, so we can tell it to <strong><code>Assume</code></strong> that the variable will never be null:</p> <pre><code>void DoSomething() { var example = OtherLibrary.FetchString(); Contract.Assume(example != null); if (ContainsAnX(example)) Console.WriteLine("The string contains an 'X'."); else Console.WriteLine("The string does not contain an 'X'."); } </code></pre> <p>Now this will be okay with the static checker. If you have runtime contracts enabled, the Assume will also be checked at run time.</p> <p>Another case where you might need Assume is when your preconditions are very complex and the static checker is having a hard time proving them. In this case you can give it a bit of a nudge to help it along :)</p> <p>In terms of runtime behavior there won't be much difference between using Assume and Requires. However, results with the static checker will differ greatly. The meaning of each is different as well, in terms of who is responsible for the error in case of failure:</p> <ul> <li>Requires means that <strong>the code which calls this method</strong> <em>must</em> ensure the condition holds.</li> <li>Assume means that <strong>this method</strong> is making an assumption which should always hold true.</li> </ul>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload