locked
Code Contracts Community

    Question

  • Hi,
    Is there a place (forum, mailing list, ...) to get in touch with people behind new DbC System.Diagnostics.Contracts library? After watching the PDC sessions, I would really like to ask a few questions about it, and since I found none, I was hoping someone reading this forum might help.
    Thanks very much.
    Martin
    -md-
    Wednesday, November 05, 2008 5:03 PM

Answers

  • Hi! I'm from the Code Contracts team. We don't have a permanent forum yet, but are in the process of setting one up. Until then we will monitor this forum, so feel free to use it. (After all, we're somewhat friendly with the Pex folks!)

    If you'd prefer to just send mail to us, then you can use a one-way mailing list (codconfb _at_ microsoft _dot_ com) that we've set up. You can send mail to it, but unfortunately you will not receive messages sent to that alias.

    Looking forward to hearing from you!

    Mike Barnett
    Wednesday, November 05, 2008 10:49 PM
    Moderator
  • Hi Martin,

    these are great questions, and this is one of the most tricky issues we've been grappling with. There are several ways you can solve this dilemma:

    1. Use RequiresAlways, and in your Release build, still run the contract rewriter as a post-build step. This way, you can customize the behavior to your desire.

    2. Use the legacy requires form, namely "if (!cond) throw ....". In order for the tools to understand that these are actually preconditions, you have to have at least one more contract following them, either another Requires, or an Ensures. If not, use CodeContract.EndContractBlock(); to delimit the end of these legacy requires. This way, you get them in your Release builds with full customization, and yet, the tools pick them up as requires.
          
    The main difference between 1 and 2 is whether or not you are willing to ship bits that went through the contract rewriter. The advantage of 1 is that you get inheritance of the requires, and the rewriter can stick the "condition string" into the binary for you.

    -MaF

    • Marked as answer by Martin Dvorak Friday, November 07, 2008 4:32 PM
    Friday, November 07, 2008 4:14 PM
    Moderator

All replies

  • Hi! I'm from the Code Contracts team. We don't have a permanent forum yet, but are in the process of setting one up. Until then we will monitor this forum, so feel free to use it. (After all, we're somewhat friendly with the Pex folks!)

    If you'd prefer to just send mail to us, then you can use a one-way mailing list (codconfb _at_ microsoft _dot_ com) that we've set up. You can send mail to it, but unfortunately you will not receive messages sent to that alias.

    Looking forward to hearing from you!

    Mike Barnett
    Wednesday, November 05, 2008 10:49 PM
    Moderator
  • Hi Mike & All,

    Very much liking the code contracts having watched your video. Coincidentally I was looking into design by contract and Eiffel a few weeks back.

    One thing that stood out to me watching the video is the fact that the code contracts are included in the body of methods which clutters the method and also looks very much like run time code. It would seem more natural to have the contracts as part of the interface/signature of the method or even as attributes as it is declarative and I don't think the current syntax makes that clear.

    I wonder if you could comment on this. Is this just a bit of kludge to get it in the framework rather than the language? Are the plans to make it part of the languages (even it is quietly using the framework assemblies)? Could it use attributes instead? Or do you think there's a good visual reason for having it as part of the method body?

    Thanks,
    LJ.


    Friday, November 07, 2008 1:25 AM
  • Hi Mike, thanks for info. I've got one question regarding preconditions. If I understand it correctly, they can be used instead of argument checking if ... throw ArgumentException code blocks. Also, if I understand it correctly, runtime checking is supposed to be turned off for release builds, which makes sense because the performance penalty could be quite huge and a lot of checks should be unnecessary if the code is properly tested. However, there is a group of checks which should stay in release builds too - e.g. checks of arguments of public and protected methods/properties in reusable class libraries. I understood that CodeContract.RequiresAlways() method is supposed to be used in these situations, however this method calls Debug.Assert(false) by design and there is no way to change this behavior if binary rewriter is not used (and it isn't in release builds). That is a problem because Debug.Assert() does not throw catchable exception which means that there is no way for clients of class libraries which use CodeContract.RequiresAlways() to do argument checking to recover from the error nor to at least catch it and write to a log file whatever.

    It would be great if it was possible to use binary rewriter for release builds too, but without CONTRACTS_FULL nor CONTRACTS_PRECONDITIONS being defined, so that RequiresAlways() calls could be rewritten to calls to methods in custom class. It does not seem to be possible with current VS2008 plugin. Maybe, it would even make sense to have an option to automatically remove Requires() calls from internal and private methods/properties but keep them and rewrite them on public and protected ones for release builds.

    Martin

    -md-
    Friday, November 07, 2008 12:06 PM
  • Hi Martin,

    these are great questions, and this is one of the most tricky issues we've been grappling with. There are several ways you can solve this dilemma:

    1. Use RequiresAlways, and in your Release build, still run the contract rewriter as a post-build step. This way, you can customize the behavior to your desire.

    2. Use the legacy requires form, namely "if (!cond) throw ....". In order for the tools to understand that these are actually preconditions, you have to have at least one more contract following them, either another Requires, or an Ensures. If not, use CodeContract.EndContractBlock(); to delimit the end of these legacy requires. This way, you get them in your Release builds with full customization, and yet, the tools pick them up as requires.
          
    The main difference between 1 and 2 is whether or not you are willing to ship bits that went through the contract rewriter. The advantage of 1 is that you get inheritance of the requires, and the rewriter can stick the "condition string" into the binary for you.

    -MaF

    • Marked as answer by Martin Dvorak Friday, November 07, 2008 4:32 PM
    Friday, November 07, 2008 4:14 PM
    Moderator
  • Hi MaF,
    thank you for your answer. I like the first solution but I found no way how to do it with current VS2008 Contracts plugin. I guess I could add binary rewriter to release build manually by adding post-build step or by modifying project build file. Nevertheless it would be great to be able to set it on Code Contracts tab in project properties.

    The possibility of having condition string added to the binary by the rewriter is great and it's a feature I've been looking for for a long time. This way it is no longer necessary to write custom error messages because the condition string says it all and together with stack trace it is all the information that is needed to locate the check in the source code. Also the source code is much cleaner now with all those if ... throw checking blocks gone. I have created alias K = System.Diagnostics.Contracts.CodeContract by using directive to make it even shorter and am very satisfied with the result. I guess that the library design as it is right now is near maximum of what can be done without extending language syntax.

    One more thing which would be absolutely great comes to my mind. Have you considered extending the rewriter to be able to rewrite this

    public void Insert( int index, object item )

    {

      K.Requires( index >= 0 );

      K.Requires( index <= Count );

      K.Requires( item != null );

     

      ...

    }


    to something like this?

    public void Insert( int index, object item )

    {

      if( !( index >= 0 ) )

        CustomReporter.ConditionFailed( "index >= 0", new ConditionVariable( "index", index ) );

      if( !( index <= Count ) )

        CustomReporter.ConditionFailed( "index <= Count", new ConditionVariable( "index", index ), new ConditionVariable( "Count", Count ) );

      if( !( item != null ) )

        CustomReporter.ConditionFailed( "item != null", new ConditionVariable( "item", item ) );

      ...

    }


    ConditionFailed method of CustomReporter class is defined like this:

    public static void ConditionFailed( string condition, params ConditionVariable[] vars )

    It would allow CustomReporter class to include values of variables used in the condition in the error message which would be invaluable both for development-phase debugging and solving bugs from bug reports. If some variables used in conditions could contain sensitive information (like passwords), CustomReporter class could filter them out using custom logic, or there would be another override or parameter saying "do not dump variable values for this condition".
    I know this is not an easy task for the rewriter to do (parsing the condition etc.) but the outcome would be really rewarding.

    Martin


    -md-
    Friday, November 07, 2008 5:57 PM
  • Hi Martin,

    thanks for the feedback and suggestions. Let's talk about the VS plugin first. You are of course right that the UI currently does not directly support my solution 1. Ie., you have to write your own post build step, which is silly. We should make it an option on the UI to run the rewriter without defining the condition CONTRACTS_FULL symbol, thereby obtaining only the RequiresAlways preconditions. In fact, we could extend it to also support just preconditions, as they have a separate symbol on them (CONTRACTS_PRECONDITIONS).

    I'll put this down as a todo.

    As for the CustomReporter suggestion, I see why this could be useful. We currently don't give you a programmatic way to look at the actual condition. Presumably, if the code contracts take off, we will eventually have reflection support, so that it should be possible to obtain the condition that failed via reflection.

    We currently try to rewrite the assembly in a minimal way, as we want to minimize the risk of breaking the original code. What you are suggesting is definitely possible, but not something we are planning at the moment.

    -MaF
    Saturday, November 08, 2008 12:35 AM
    Moderator
  • Hi LJ,

    Clearly, having 1st class language support, like Eiffel, for contracts would be sweet. Our approach is not precluding this in the future. In fact, if any of the .NET languages want to add syntax for it, they can, and just emit the format we have standardized on and the tools will pick it up.

    -MaF

    • Proposed as answer by Laughing John Tuesday, November 11, 2008 1:18 AM
    Saturday, November 08, 2008 12:41 AM
    Moderator
  • Hi,

    I've found what I think is a bug in ccrefgen.exe.  Is this the place to report it?

    Thanks,
    Gabriel

    Monday, November 10, 2008 4:30 AM
  • Thanks Maf - it looks like a brilliant tool, but the syntax just doesn't look 'right' to my eye (could just be me), so I was curious. It's encouraging to know it may get incorporated in the actual interface in the future.

    Keep up the good work, I think MS had some really positive stuff for us from watching the PDC videos.
    Tuesday, November 11, 2008 1:22 AM
  • I attended the PDC session on this and was very encouraged by what I saw.  One usage that doesn't appear to be addressed is manually checking invariants in release builds.  In particular, I'm thinking about user input scenarios.

    It seems that some contract invariants overlap with business rules about a given object that may be defined.  When a user is modifying an object, you typically have to validate the object based on some set of rules.  Rather than having to duplicate your invariants in your other rules framework, it would be nice to be able to programmatically say "check my invariants now".  The flow would be roughly: get/create object, apply user supplied values, check invariants, if check fails display message to user else proceed to other validation, etc.   All that would be required from the contracts library is the ability to say "Contracts.SatisfiesInvariants(objectToCheck)" or something similar (Try pattern? throw on violate?)

    From the PDC session it appears that the contracts aren't present in the release build, but are available in a parallel assembly.  I don't know if those contracts are in an executable form, however.

    My goal here is to leverage the invariants already defined and not have to duplicate them in domain validation logic.
    Wednesday, November 12, 2008 8:55 PM
  • Please send all bug reports on the tools to "codconfb" _at_ "microsoft" _dot_ "com". That way we will be sure to see it.

    Thanks!

    Mike
    Thursday, November 13, 2008 9:10 PM
    Moderator
  • Thanks! The object invariant is just a method that you add to your class, so you are free to call it from anywhere in your code. But now that I say that, I realize that the calls to Contract.Invariant *within* that method will not be defined unless you define the symbol that defines *all* contracts, which means you'd also have to use the binary rewriter. But I'm not completely sure why youl would want to explicitly call an object invariant. Usually those contracts express the internal constraints which define when your object is in a good state. If your code is correct, why would you need to check that at runtime other than during testing?
    Thursday, November 13, 2008 9:15 PM
    Moderator
  • Let's assume we are in an edit scenario.  The user is loading up an object, making some changes, and saving it again.  The usual process is something like:
    1.  Load the object (I know the object is in a good state here)
    2.  Collect the user input relating to changes (maybe from a form post in a web scenario)
    3.  Apply the user input to the loaded object (note that the object may be in an invalid state here)
    4.  Check that the user entered valid data
    5.  Save the object

    For a trivial example, assume the user types in a percentage and we want to validate it is between 0 and 100.  The user might type in 200, so the object after step 3 would be invalid.  Step 4 is usually accomplished via some coded or declarative validation rules.  It would be nice, however, to reuse the contracts we've already defined (invariants) to check portions of this.

    Another way of putting it is that I agree that if the code is correct the invariants should always hold.  Therefore, for my code to be correct, I must check all user input against a set of validation rules that ensure my invariants aren't violated.  Rather than having this check be something I hand code (and that will duplicate knowledge already contained in the contract, in this case, that Percentage must always be between 0 and 100), I'd like to be able to reuse the contracts to help me do the check.
    Thursday, November 13, 2008 9:51 PM
  • Hey Mike and all,

    I watched your PDC presentation with great interest, having followed the progress of Spec# enviously for quite some time.  I am happy to see some of the results of that research making its way into the BCL.  Congratulations on that!

    I’ve installed and played around with the latest version of CodeContracts (CodeContracts9.msi) - it is excellent stuff. My question... As FxCop already does a lot of static analysis, and provides an easily extensible framework for custom rules, have you considered making the CodeContracts checks available as custom rules through FxCop(FxCopSdk/Microsoft.Cci...) instead of the current cccheck, etc?  This would buy you a lot of nice free VS integration (ability to set specific rules as errors/warnings/none, help text/urls for certain issues, etc), and reduce the overhead of having two separate but similar static analysis tools needing to run for those who already use FxCop and want to take advantage of code contracts.

    Keep up the good work!

    Tuesday, November 25, 2008 4:06 PM
  • Hi, is it possible to have a 'ContractClassFor' a generic interface? I mean something like this:

        [ContractClass(typeof(ContractForIStack<T>))]
        public interface IStack<T>
        {
           ....
        }

        [ContractClassFor(typeof(IStack<T>))]
        public class ContractForIStack<T> : IStack<T>
        {
            ....
        }

    The compiler complains that 'an attribute argument cannot use type parameters'

    Thanks a lot,

    Giacomo


    Monday, December 01, 2008 3:05 PM
  • Hi Giacomo,

    Can you post this question as a new thread?
    Thanks,
    Peli
    Jonathan de Halleux
    Monday, December 01, 2008 7:05 PM
    Owner