Comments on Moserware: Borrowing Ideas From 3 Interesting Internal Clas...

Greg: very interesting! Thanks for the info. I'll ...

2008-01-28T22:10:00.000-05:00

Greg: very interesting! Thanks for the info. I'll have to try it out.

spec# errors (through boogie) can also show up as ...

2008-01-28T19:38:00.000-05:00

spec# errors (through boogie) can also show up as warnings ... its just a matter of enabling it in your project...

To do this right click on your project and go to properties ... then go to build ... under misc there is an item called "RunProgramVerifier" it is set to false by default, set it to true and off you go.

You might also want to try RunProgramVerifierWhileEditting which will incrementally run it and give you squiggly lines while you type.

Greg: Thanks for the info! I hadn't actually tried...

2008-01-23T18:51:00.000-05:00

Greg: Thanks for the info! I hadn't actually tried running spec# with an error, but it's good to know.

I'm also curious how far Boogie's help goes with projects like Pex. Something like Spec# for compiler errors and Pex/Boogie for warnings.

Jeff wrote:

"t's not much of a leap to go f...

2008-01-23T15:26:00.000-05:00

Jeff wrote:

"t's not much of a leap to go from (to use your example)

public virtual void CopyTo(Array! array, int index) {...}

to looking at the call sites like

al.CopyTo(null, 0)

and throwing a compile time error saying that this violates the contract. That is really cool stuff."

You do realize spec# already does *exactly* this ... the "boogie" portion of spec# is a full theorem prover and does give errors at compiler time.

Cheers,

Greg

Hi Jeff,

Thanks for a very interesting and ...

2008-01-19T03:41:00.000-05:00

Hi Jeff,

Thanks for a very interesting and worthwhile post. And thanks also for your related comments at my blog (to which I replied BTW).

These classes definitely look like placeholders to help with assembly re-writing tools (which I presume is what Spec# is, considering the Conditionals on some of the methods).

Even if the classes were publicly accessible, they wouldn't be truly DBC because they lack two critical components of DBC: inheritable constraints and before/after comparisons that allow you to confirm that you upheld your end of the contract.

Inheritable constraints are what's missing from the implementation I blogged about, and it's a major flaw, because you only have to override one of my methods to be freed from all the constraints I placed in my original class or interface.

I'm still looking for a way around the 'no lambdas or generics in attributes' restriction on .NET 3.5. If you find a way round it, let me know!

Cheers

Andrew Matthews

Phil: this is more or less the idea that Spec# bri...

2008-01-16T20:22:00.000-05:00

Phil: this is more or less the idea that Spec# brings. It seems that the Eiffel folks have been doing this for years in terms of the "requires"/"ensures" pattern.

After reading more on Design by Contract and looking at Spec#, a cool glimpse of the future came into my mind. Detecting bad parameters at compile time.

It's not much of a leap to go from (to use your example)

public virtual void CopyTo(Array! array, int index) {...}

to looking at the call sites like

al.CopyTo(null, 0)

and throwing a compile time error saying that this violates the contract. That is really cool stuff.

You might also want to check out Wes's support for specifications via statements embedded in comments in his upcoming NStatic tool.

Interesting stuff.

A thought occurred to m...

2008-01-16T18:42:00.000-05:00

Interesting stuff.

A thought occurred to me while reading through this. What if we could decorate our parameters for common scenarios such as nulls. To guard against a null reference you could use a suffix in a similar way to how ? can be used for nullable value types.

For example, let's use an exclamation point to guard against null parameters:

public virtual void CopyTo(Array! array, int index) { ...

So if array is null it would throw an exception.

Taking this a bit further, a double exclamation could guard against null or empty strings:
public virtual void Foo(String!! myString) { ...

Not saying this is a good idea, just that it's interesting to think about.

Phil

tweez: Thank you very much for your comment!

2008-01-16T07:46:00.000-05:00
tweez: Thank you very much for your comment!

I hadn't seen the link you mentioned before. It seems that the author of that one had similar goals. I like the idea of possibly adding a "Guard.ArgumentEnsure(bool condition, string paramName, Exception exceptionToThrowIfConditionFails)" with a simplified verision that just throws an ArgumentException.

Thanks for letting me know about things not showing up well in FireFox. I manually edited the HTML to add a border around the code. I'll do a bit more searching on how to best render code. I have been using the "Copy Source as HTML" plugin, but there's probably a better way.

This is the one I'm using. It's the guard principl...

2008-01-16T01:39:00.000-05:00

This is the one I'm using. It's the guard principle...: Design by contract.
http://www.codeproject.com/KB/cs/designbycontract.aspx

ps: Your blog doesn't show correct in FF..

Comments on Moserware: Borrowing Ideas From 3 Interesting *Internal* Clas...