« Lang.NET Symposium | Main | Research Pipeline »

August 01, 2006

Comments

Judah

I've been subscribed to the Spec# mailing list for quite some time. In that time, I've seen some real world issues that come in to play.

The Spec# verifier tool, Boogie, is sophisticated, but doesn't go too deep in some situations. IIRC, the something like the following code passes verification:

object foo = new object();
SetFooToNull(foo);
foo.Bar();

Some seemingly simple things like that caught my eye and made me wonder how useful such a tool really is.

Spec# also introduces non-null types, using the exclamation point syntax:

string! nonNullString;

While this seems like a good idea, there's a whole host of problems related to static initilization of non-null types, not to mention a lot of extra effort and wide code changes to change something from a regular reference type to a non-null type. There's so many extra pieces of code required and so many gotchas to verify these things work, I almost question whether it's truely worth the effort.

I also noticed whilst watching the mailing list that many people hit gotchas--for example, simple arithmetic operations--that that the Spec# complier doesn't or can't verify, so consumers have to fudge it by telling the compiler, "assume this is gonna be less than 10" or whatever happens to be your assumption. In other words, often times, your Spec# annotations will contain annotations basically reverting you back to regular C#.

Another things that raises eyebrows for me is that the pre- and post- conditions introduced by Spec# can call arbitrary methods, dubbed "Pure" methods. These "pure" methods are decorated with the Pure attribute...all that sounds fine. But the developer must guarantee that Pure methods don't modify any state. While that sounds reasonable, aren't we running in circles? Here we're introducing all sorts of burdens on developers in order to force them to write verifiable programs, but then in many parts of the software we are crossing our fingers and hoping they don't make false assumptions about some result (in order to "trick" the Spec# compiler into allowing something to happen, as described earlier), or by hoping the developer doesn't modify state in pure functions. Seems like we're doing a bit of backtracking here.

I suppose, though, that if Spec# results in your code having fewer bugs, it may be worth it in the long run. More time investment writing code up front, but less time fixing it in the long run.

"We are investigating annotation inference techniques"

I believe Spec# has something similar to "annotate" the entire .NET framework class library, giving it non-null types, pre- and post-conditions, etc.

The comments to this entry are closed.

My name is Wesner Moise. I am a software entrepreneur developing revolutionary AI desktop applications. I worked as a software engineer in Microsoft Excel group for six years during the 1990s. I worked on PivotTables and wrote the most lines of code in Excel 97-- about 10 times the median developer. I have a Harvard BA in applied math/computer science and a UCLA MBA in technology entrepreneurship. I am a member of the Triple Nine Society, a 99.9 percentile high-IQ society.

December 2013

Sun Mon Tue Wed Thu Fri Sat
1 2 3 4 5 6 7
8 9 10 11 12 13 14
15 16 17 18 19 20 21
22 23 24 25 26 27 28
29 30 31