Code Contract to prevent duplicates on list

Question

I'm currently checking with this contract that the parameter and the return value aren't null. Now, I need a way to check that no matter what branch of the switch it takes then the resulting IEnumerable must not have duplicates on its code values. Is this possible using code contracts. I try to use the Contract.ForAll but with no luck.

internal static IEnumerable<MenuItemAction> GetMenuActions(MenuItem menuItem)
{
    Contract.Requires(menuItem != null);
    Contract.Ensures(Contract.Result<IEnumerable<MenuItemAction>>() != null);

    switch (menuItem.Code)
    {
        case 0:
            return new MenuItemAction[3] { 
        new MenuItemAction(){Code = 0, Label = "."}, 
        new MenuItemAction(){Code = 1, Label = ".."}, 
        new MenuItemAction(){Code = 2, Label = "..."}
    };
        case 1:
            return new MenuItemAction[2] { 
        new MenuItemAction(){Code = 3, Label = "."}, 
        new MenuItemAction(){Code = 4, Label = ".."}
    };
        case 2:
            return new MenuItemAction[2] { 
        new MenuItemAction(){Code = 5, Label = "."}, 
        new MenuItemAction(){Code = 6, Label = ".."}
    };
        default: return null;
    }
}

Answer 1

Try

Contract.Ensures(
    Contract.Result<IEnumerable<MenuItemAction>>() != null &&
    Contract.Result<IEnumerable<MenuItemAction>>().Count() == 
        Contract.Result<IEnumerable<MenuItemAction>>()
           .Select(m => m.Code)
           .Distinct()
           .Count()
);