Writing a CodeContract for an Activity - How can Contract.Requires / Ensures enforce InArgument<T>, OutArgument<T>, ActivityContext ???

Question

As lead developer, I would like to create some CodeContract enforced activities for my dev team to implement.

I want to specify preconditions for InArgument<T> properties, and postconditions for Result<T>

Given a canonical AddActivity, I would like it to implement a contracted interface using System.Diagnostics.Contracts:

 

    // the contracted interface:
    [ContractClass(typeof(AddActivityContract))]
    interface IAddActivity
    {
        InArgument<int> A { get; }
        InArgument<int> B { get; }
        OutArgument<int> Result { set; }
    }
 
    // the Activity:

    public class AddActivity : NativeActivity<int>, IAddActivity
    {
        public InArgument<int> A { get; set; }
        public InArgument<int> B { get; set; }
 
        protected override void Execute(NativeActivityContext context)
        {
            var a = context.GetValue(A);
            var b = context.GetValue(B);
 
            // the line developer would implement the following to pass the contract. (obviously trivial for canonical add).
            var result = a + b;
 
            Result.Set(context, result); 
        }
    }

My problem is, how do I get the contract class to work with NativeActivityContext ?

I tried the following, but its not checking pre & post conditions at compile time:

// the Contract:
    [ContractClassFor(typeof(IAddActivity))]
    sealed class AddActivityContract : IAddActivity
    {
        private ActivityContext context;
        public InArgument<int> A
        {
            get
            {
                Contract.Requires(0 <= Contract.Result<int>());
                return Contract.Result<int>();
            }
        }
        public InArgument<int> B
        {
            get
            {
                Contract.Requires(0 <= Contract.Result<int>());
                return Contract.Result<int>();
            }
        }
 
        public OutArgument<int> Result
        {
            set
            {
                Contract.Ensures(A.Get(context) + B.Get(context) == value.Get(context));
            }
        }
    }

How can I make this work ?

Answer 1

Unfortunately I don't think this is going to work, the reason being that (AFAIK) Code Contracts don't specifically support WF4, and especially don't know about activity data flow rules - they only know about regular CLR method arguments and data flow of those. If there's a CodeContract discussion group perhaps my suspicions can be confirmed by parties there.
Tim

Answer 2

This isn't going to work because InArgument<T> is a wrapper over a value that is accessible only via a context.  In the OutArgument example above you have context but it isn't clear where that comes from.  There is only one place in your code where the context is valid and is in the override of the execute method.  The static checking of Code Contracts won't be able to help here.  You can throw an exception at runtime if you get an invalid value.

---

Ron Jacobs Sr. Program Manager, AppFabric Development Platform (WF/WCF)

Answer 3

Fair enough - it would be a great feature in V5.0 though!