Greg Young [MVP]

Sponsors

The Lounge

Syndication

Recent Posts

Tags

View more

News

Archives

Advertisement

Greg Young [MVP] » Spec# coming soon to a framework near you?
Images in this post missing? We recently lost them in a site migration. We're working to restore these as you read this. Should you need an image in an emergency, please contact us at imagehelp@codebetter.com
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) (doubleBitsDevil & 240)) >> 4));
}

 

Somebody at Microsoft has really made my DAY!!!

 


 

 

 

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

Posted Wed, Nov 21 2007 6:34 PM by Greg

[Advertisement]

Comments

JD Conley wrote re: Spec# coming soon to a framework near you?
on Wed, Nov 21 2007 7:04 PM

Freaking awesome! Too bad they're internal...

Peter Ritchie wrote re: Spec# coming soon to a framework near you?
on Wed, Nov 21 2007 8:21 PM
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...
Colin Jack wrote re: Spec# coming soon to a framework near you?
on Thu, Nov 22 2007 3:21 AM

Nice.

nick wrote re: Spec# coming soon to a framework near you?
on Thu, Nov 22 2007 8:04 AM
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
Greg wrote re: Spec# coming soon to a framework near you?
on Thu, Nov 22 2007 1:41 PM

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

Jason Haley wrote Interesting Finds: November 22, 2007
on Thu, Nov 22 2007 2:52 PM
mccoyn wrote re: Spec# coming soon to a framework near you?
on Fri, Nov 23 2007 1:40 PM

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.

Jeremy D. Miller -- The Shade Tree Developer wrote TDD/BDD and Design by Contract: I don't really see any conflict between the two
on Tue, Dec 11 2007 8:54 AM

I found an interesting link today from Mario Gleichmann called Test Driven Development and Design By

Peter's Gekko wrote Tests on Dutch .NET community read green
on Mon, Dec 17 2007 4:38 AM

Friday 14th Dutch user Group SDN had a full day meeting. The SDN has a very long history, it started

Patrick Smacchia [MVP C#] wrote Attributes as a mean to partition code
on Fri, Mar 14 2008 3:18 PM

On top of things Code Query Language users where asking for, was the condition HasAttribute . I am glad

Peter's Gekko wrote Tests on Dutch .NET community read green
on Thu, May 29 2008 9:54 AM

Friday 14th Dutch user Group SDN had a full day meeting. The SDN has a very long history, it started

Add a Comment

(required)  
(optional)
(required)  
Remember Me?