Sponsored By Aspose - File Format APIs for .NET

Aspose are the market leader of .NET APIs for file business formats – natively work with DOCX, XLSX, PPT, PDF, MSG, MPP, images formats and many more!

Spec# coming soon to a framework near you?

Snooping through 3.5 now that its in production I found something I was REALLY hoping to see … Anyone up for guesses on why Microsoft.Contracts made it into System.Core? :)

 

 

 

 

 Not ONLY this but parts of the framework (oddly the new parts) ACTUALLY USE the contracts!!!

 

 [Serializable, StructLayout(LayoutKind.Sequential), Immutable, ComVisible(false)]
internal struct BigInteger : IFormattable, IEquatable<BigInteger>, IComparable<BigInteger>, IComparable

Yes YES YES !!! IMMUTABLE …. mmm so yummy!

 

 [Pure]
public static bool operator >(BigInteger x, BigInteger y)
{
    return (Compare(x, y) > 0);
}

And finally …

private static ushort Exponent(byte[] doubleBits)
{
    Contract.Requires(doubleBits.Length == 8);
    return (ushort) ((((ushort) (doubleBits[7] & 0x7f)) << 4) | (((ushort) (doubleBits[6] & 240)) >> 4));
}

 

Somebody at Microsoft has really made my DAY!!!

 

 

 

 

Very soon me thinks … spec# will be coming to a framework near you!! 

This entry was posted in Uncategorized. Bookmark the permalink. Follow any comments here with the RSS feed for this post.

6 Responses to Spec# coming soon to a framework near you?

  1. mccoyn says:

    I think what Spec# really needs is framework support. Not just the native types (String, Array), but also stuff like Windows.Forms. I’ve been experimenting with it for a couple weeks and I find I have to write assume statements all over the place. Its becoming a habit, which means I don’t take a moment to think about how the assumption might break the application. I think the value of Spec# is in those moments of thought.

  2. Greg says:

    Nick … can you define “properly”?

    As of now I personally don’t like the decisions made by spec# when it comes to pre/post conditions and inheritance. It is quite strict in that I can’t strengthen a contract when overriding … I understand why this decision was made (the contracts should be the same if I am using them in a polymorphic fashion so the prover can actually prove no runtime contract violations) but it doesn’t ‘feel’ natural to me…

    I had seen some of those tools for generating tests automagically … looks pretty cool.

    “. Now, this makes lots of unit testing (but not all) redundant. Look at your current unit tests. Most will be set up test cases that match the preconditions”

    I have been saying exactly this for a long time (in the code bases I have analyzed generally 60-70% of lines of test code are testing just this). I think however the generation of tests will go away … I think instead we will try to version our contracts (using some tool) and watch changes in those contracts over time…

    Cheers,

    Greg

  3. nick says:

    If it works properly with inheritance, then we are on the way.

    Editors need to be clever so they can fold the implementation out of the way leaving just the assertions.

    http://research.microsoft.com/Pex/ Pex is an example of automated testing from MS that’s interesting.

    http://se.inf.ethz.ch/people/arnout/arnout_rousselot_meyer_test_wizard.pdf describes a project that looks at the contracts and generates the tests automatically.

    The two approachs are different but share lots of features that are interesting.

    Now, this makes lots of unit testing (but not all) redundant. Look at your current unit tests. Most will be set up test cases that match the preconditions, execute, then assert the post conditions. Shock horror, its just assertions put outside the class, run just once.

    DBC means you run continually your testing of your contracts until you turn them off. Much more extensive.

    Combine that with some of the tools above, and you’ll get much more information such as redundant contracts or missing contracts

  4. Interesting, I wonder if that has anything to do with the ImmutableAttribute in Joe Duffy’s recent blog http://www.bluebytesoftware.com/blog/CommentView,guid,58392086-9f4c-4e0c-82ff-05b090c09f04.aspx where he says “Imagine we had an ImmutableAttribute.” I wonder if the 3.5 CLR uses it at all…

  5. JD Conley says:

    Freaking awesome! Too bad they’re internal…

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>