locked
Just static analysis RRS feed

  • Question

  • Thanks for this wonderful piece of technology.

    How can we structure our code so as to reap maximum benefits from static analysis? What are the constructs to use, which ones do we avoid?

    Thanks,
    Dejan
    Thursday, February 26, 2009 8:30 AM

Answers

  • Hi Dejan,

    I wish I could give you a clear cut answer. Unfortunately, it's not that easy due to limitations in the current implementation of the checker which we are actively improving.
     
    Nevertheless, here are some general guidelines that should help:

    1. Write simple code. Simple API's have simpler contract and will be easier to check.
    2. Write post-conditions (ensures) on methods. This allows you to transmit information about the post state at a call-site, which likely helps prove further obligations after the call.
    3. Don't go overboard with enabling too many checks at once.
    4. Focus on a small part of the code initially using [CodeVerification(true/False)] to limit the scope of analysis.

    Limitations you'll run into:
    1. Many framework library methods need post-conditions. We are actively filling these in, but there are many that don't have them.
    2. The current release has a bug in that [Pure] attributes are not seen from other assemblies. Thus you'll get false warnings about impure methods being used in contracts. This should be fixed in the next release.
    3. The checker only understands unary method predicates. More complicated predicates are simply ignored. We'll try to fix this by the summer.

    Ways to help the checker:
    1. If the checker can't prove something at a particular point, try to put an assertion prior to that point where you think something should be provable. Do this repeatedly, moving the assertion up in the code until you find where infomation in missing. This will often be a missing post-condition on a call, or a pre-condition.
    2. If you are still stuck, use Contract.Assume. This tells the static checker "Believe me, this should be true". The checker then uses this assumption without trying to prove it. It still will be checked at runtime in debug builds.
    3. If nothing else works, use [ContractVerification(false)] on the method to shut it up for now. You can use the attribute on classes and assemblies as well. It applies to the entire hierarchy where it is on. You can flip the default again and again by adding [ContractVerification(true)] at another level.

    And please, ask questions when you get stuck.

    Cheers, -MaF (Manuel Fahndrich)
    Saturday, February 28, 2009 7:10 AM