C# Design by Contract: How to Guarantee method and function

I recently started using design by contract with my project. I have some questions regarding on how to guarantee method and function.

public static void SaveAttachment(Outlook.MailItem _mailItem, string saveTo)
    {
        Contract.Requires<ArgumentNullException>(_mailItem != null);
        Contract.Requires(_mailItem.Attachments.Count > 0);
        Contract.Requires(!String.IsNullOrEmpty(saveTo));            

        string attachLink = "<file://{0}&开发者_如何学Gogt;";
        StringBuilder sBuilder = new StringBuilder();
        try
        {
            foreach (string fp in saveAllEmailAttachmentsThenReturnSavedFilePathList(emailAttachmentList(_mailItem), saveTo))
            {
                sBuilder.Append(String.Format("Attachment saved: " + attachLink, fp) + Environment.NewLine);
            }
            _mailItem.Body = sBuilder.ToString() + _mailItem.Body;
            _mailItem.Save();                
        }
        catch (Exception ex)
        {
            LogErrorMessage(ex);
        }            
    }

As you can see the above method will save email attachment and it make sure the mail item that is pass in is not null and have attachment. However, how do i guarantee that this method will do what it suppose to do.

On Function:

public static List<Outlook.MailItem> SelectedMail(Outlook.Selection selectedItems)
    {
        Contract.Requires(selectedItems.Count > 0);
        Contract.Ensures(Contract.Result<List<Outlook.MailItem>>().Count > 0);

        List<Outlook.MailItem> selectedMails = new List<Outlook.MailItem>();
        foreach (object obj in selectedItems)
        {
            if (obj is Outlook.MailItem)
            {
                selectedMails.Add((Outlook.MailItem)obj);
            }
        }

        Contract.Assume(selectedMails.Count > 0);
        return selectedMails;
    }

What if the selectedItems have no mailitem? if I write contract ensures this way would it cause error on selected email that have no attachment.

Sorry, I'm new to this paradigm. I want to learn it so I don't have to write safe guard code with if-else.

---

For your specific case, I see two possibilities:

1. The Ensures requirement is false and it's valid for there to be a 0 Count result.

2. You have an additional runtime requirement that cannot be reasonably expressed as a Contract, since it's not something that a static checker could hope to prove and so you would not want to Assert it. This is the case where you probably just want to check the condition at runtime and throw an Exception.

If you find yourself wanting to express a very complex requirement as part of a Contract (or even to throw an Exception), you might want to reconsider your design and why this complex requirement exists. Will the users of your method be able to remember and understand the requirement? Is there some other way you can encapsulate the behavior so that the requirement is expressed more clearly?

---

Your code, with the .Assume() will probably not give warnings.

But you need an Assume() , a cop-out, because the static verifier cannot look far enough back into the source of your data. Assume is where you take responsibility by inserting a piece of 'outside' information.

As long as you keep the .Requires active this is OK. The static checker verifies the rest of your logic assuming there is valid data.

But note that in practice I would do it a little different:

    public static List<Outlook.MailItem> SelectedMail(Outlook.Selection selectedItems)
    {
        Contract.Requires(selectedItems != null);    //always a good idea
        Contract.Requires(selectedItems.Count > 0);

        // can't promise this
        // Contract.Ensures(Contract.Result<List<Outlook.MailItem>>().Count > 0);  

        List<Outlook.MailItem> selectedMails = new List<Outlook.MailItem>();
        foreach (object obj in selectedItems)
        {
            if (obj is Outlook.MailItem)
            {
                selectedMails.Add((Outlook.MailItem)obj);
            }
        }

        // and then w/o the promise we don't need this
        // Contract.Assume(selectedMails.Count > 0);
        return selectedMails;
    }


    void SomeMethod()
    {
       var selected = SelectedMail(...);
       if (selected.Count > 0)
          SaveAttachment(selected, "file")
       else
          // you need a plan here anyway

    }

This would verify without an Assume()

---

Well, for the second code snippet you could try:

Contract.Requires(Contract.Exists(selectedItems, x => x is Outlook.MailItem));

EDIT: Gah - if Outlook.Selection implements IEnumerable but not IEnumerable<T>, that won't work :(

I'm not sure how well such a contract can be checked by the static compiler, admittedly...

By the way, your method body can be reduced in size really easily:

return selectedItems.OfType<Outlook.MailItem>().ToList();

Isn't LINQ lovely? :)

I'm not quite sure what you're trying to guarantee in the first piece of code... I don't think you can really express the "it gets saved" part, to be honest.