{"id":307580,"date":"2007-08-14T08:00:09","date_gmt":"2007-08-14T15:00:09","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/?p=307580"},"modified":"2016-10-18T22:41:00","modified_gmt":"2016-10-19T05:41:00","slug":"spec-producing-high-quality-software","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/spec-producing-high-quality-software\/","title":{"rendered":"Spec#: Producing High-Quality Software"},"content":{"rendered":"

By Rob Knies, Managing Editor, Microsoft Research<\/em><\/p>\n

Modern-day software development is notoriously challenging. Programs have become highly complex. Customer expectations have never been higher. Meeting quality standards is increasingly difficult.<\/p>\n

Challenging, yes. Difficult, perhaps. But such hurdles are not insurmountable, as Spec#<\/a> demonstrates.<\/p>\n

Spec#, available for download (opens in new tab)<\/span><\/a>, is a programming system devised by researchers from the Programming Languages and Methods group at Microsoft Research Redmond<\/a>. The project\u2014started by Rustan Leino<\/a>, Mike Barnett<\/a>, and Wolfram Schulte\u2014attempts to streamline the development and maintenance of high-quality software.<\/p>\n

\u201cOur goal,\u201d the three write in a paper entitled The Spec# Programming System: An Overview<\/em><\/a>, \u201c[is to migrate] normally skilled programmers to a higher-integrity language.\u201d<\/p>\n

And just how do they propose doing that? Try the carrot-and-stick approach\u2014but hold the stick. Spec# is an effort to encourage programmers to add specifications to their software, to ensure that the assumptions that are made during the software-engineering process hold true. And the system\u2014consisting of the object-oriented Spec# programming language, a Spec# compiler, and the Boogie static program verifier\u2014provides incentives for the adoption of such techniques.<\/p>\n

\u201cWhat we\u2019ve tried to do,\u201d says Leino, the project lead and a principal researcher with the Programming Languages and Methods group, managed by Schulte, \u201cis think about the whole experience of the language. How do you write the programs? What sort of specifications do you include in the programs? What do you do with them?\u201d<\/p>\n

Those are the questions the Spec# project attempts to answer, but the goal is to improve the process of writing high-quality software.<\/p>\n

\u201cThe overall goal is to improve the software-engineering process,\u201d Leino says. \u201cSoftware engineering is very expensive in terms of figuring out and designing what the program should do and then actually writing the programs. There\u2019s a lot of cost in writing the programs up front to develop them initially. But a much larger cost is the maintenance of the program.<\/p>\n

\u201cWhat we\u2019d like to do is make it more cost-effective in various ways. Programmers tend to run tests, so the testing accounts for a large portion of the cost of software engineering. That is, in some sense, what we\u2019re competing with, but we\u2019re not aiming to replace testing. We just want to be able to do it in a smarter way earlier in the software-development cycle, and the way to do that is to use specifications.\u201d<\/p>\n

The idea of appending specifications to the software-engineering process is not new. Such techniques have been discussed for decades. But it\u2019s been an uphill battle to get software developers to embrace the concept of building specifications into the development model.<\/p>\n

\u201cIt takes more of a long-term view to understand why the specifications are good,\u201d Leino concedes. \u201cTypically, if you have to do a lot more up front to develop the program, then many people in the process get nervous, because they\u2019re not getting as quickly to the date when testing starts.<\/p>\n

\u201cThe idea is that if you do these things up front, it takes you longer to get to that point, but when you do, the program is in much better shape to begin with. Having the specifications in the program means that when you maintain the program, someone can come in, read the specifications, and when they make changes, you can immediately have tools that check to make sure you haven\u2019t messed up anything in the program.\u201d<\/p>\n

The concept is sound, but how can it be implemented within an environment that values go-to-market alacrity?<\/p>\n

\u201cTo communicate that benefit to the programmer,\u201d Leino says, \u201cwe must give them incentive to do it.\u201d<\/p>\n

Enter the carrot. In this instance, the incentives take three forms. The first is type checking, which occurs during program compilation.<\/p>\n

\u201cThe programmer writes the program in some language\u2014in our case, Spec#,\u201d Leino says, \u201cand then wants to translate it into something the machine can actually run. When the compiler runs, it also involves a type checker, which is a very coarse-grained way to look at the program and figure out that you\u2019re not mixing up apples and oranges, integers and Booleans.\u201d<\/p>\n

Type checking has been used in all modern programming languages, so software developers are quite familiar with that process. What Spec# offers is a way\u2014in large part due to the efforts of Manuel F\u00e4hndrich, another Microsoft Research Redmond researcher\u2014of checking for non-null types, to make sure that pointers within a program point to the objects for which they are intended.<\/p>\n

\u201cOur type system in Spec# addresses that,\u201d Leino says. \u201cWhen the compiler runs, the programmer gets that checking immediately. That, we think, is one incentive for them.\u201d<\/p>\n

Another is pre- and post-conditions, which represent contracts within a program that ensure that the routines in the program run as expected.<\/p>\n

\u201cThink of it as there\u2019s someone who\u2019s going to call a particular routine, and there\u2019s someone who\u2019s going to implement the routine.\u201d Leino says. \u201cYou have a contract sitting in between that says what the obligations of the caller are and what the obligations of the implementer are. The caller has to live up to the precondition, but then the implementer can assume that the precondition holds, because the contracts says that it does, and the implementer must establish the postcondition, and then the caller can assume that it holds upon return.\u201d<\/p>\n

In its use of such contracts, Spec# resembles the Eiffel object-oriented programming languages. Like Eiffel, Spec# provides runtime checking of preconditions and postconditions.<\/p>\n

\u201cThe programmer,\u201d Leino says, \u201cby writing down just one precondition in the entire program\u2014or two or three or 100\u2014gets the benefit of our compiler generating runtime checking. The programmer starts to benefit.\u201d<\/p>\n

The third carrot involves static program verification.<\/p>\n

\u201cThat means we\u2019re going to analyze the program mathematically to check that these specifications really always hold,\u201d Leino adds. \u201cThat process essentially means that you need to have enough specifications in the program that you can convince even a program verifier that the program is correct.<\/p>\n

\u201cThat step takes a lot more effort for the programmer, so one of our research aims is to provide as much of the boilerplate as we can and to infer things when we can and make it as easy as possible for the programmer to do that last step well. We have lots of research to do there.\u201d<\/p>\n

Leino previously worked on a similar static verifier for the Java programming language. But, he hastens to add, Spec# has leapfrogged Eiffel and Java.<\/p>\n

\u201cWhat we offer that is much stronger is the static verification,\u201d he says. \u201cI think we lead there.\u201d<\/p>\n

The Spec# project got started about four years ago.<\/p>\n

\u201cWolfram and Mike came from a background of doing runtime checking and modeling in programs,\u201d Leino says, \u201cand they wanted to see contracts in the language. I came more from the static-verification background. We noticed that we had similar interests and then started the project.\u201d<\/p>\n

Spec# is aimed at two distinct audiences.<\/p>\n

\u201cThe people who are using it now and who we would want to be using it are early adopters,\u201d Leino says, \u201csomeone who\u2019s willing to try something new, see how it works out. We have an external Spec# mailing list where we get many good questions.<\/p>\n

\u201cAnother kind of user that we want is users in academia being able to use our language and our tools in teaching, both for students to be able to put in the contracts and get a feeling for what the contracts are for, and then also taking the extra step for verifying statically.<\/p>\n

\u201cWhen specification and verification are taught at universities,\u201d he adds, \u201cthe typical way that they\u2019re taught is that you have some lectures and then you learn how to do proofs and loop invariants and pre- and post-conditions. The students do it on paper, and they prove it. They may or may not get it right, they hand it in, and a week later, someone grades it, and then it gets forgotten.<\/p>\n

\u201cWhen they take the next programming class, when they\u2019re sitting at a terminal actually writing a program, they don\u2019t necessarily associate what they did in that paper-and-pen class with the actual programming experience. We think the tools we have can connect those two, so that you both understand the things you\u2019re doing and you\u2019re getting used to putting the things in\u2014pre-conditions, post-conditions\u2014when you\u2019re writing the program.\u201d<\/p>\n

Another benefit to Spec# is the fact that the language is a superset of the popular C# programming language.<\/p>\n

\u201cIf someone is used to programming in C#,\u201d Leino says, \u201cit should be straightforward for them to switch to Spec#. The Spec# compiler accepts C# programs, since we\u2019re a superset of C#, and in Microsoft Visual Studio, you can switch to the Spec# mode, which offers some benefits.\u201d<\/p>\n

Of course, because Spec# is a research project, it doesn\u2019t offer all the bells and whistles of Visual Studio. But Spec# does offer the additional quality check enabled by the contracts.<\/p>\n

\u201cThose can be put in a C# program as just comments,\u201d Leino explains. \u201cThat means that when the C# compiler looks at the program, it ignores the comments. But when the Spec# compiler runs on the same program, it looks into the comments and treats them as if they weren\u2019t written in comments. C# programmers can download our system and choose to turn on contracts. If they do that, they can write contracts in the comments. Then, when they compile it in Visual Studio, they can first run the C# compiler, then immediately afterward run the Spec# compiler. Then they get all the whiz-bang features of C# and the benefits of our compiler.\u201d<\/p>\n

Spec# also offers runtime checking for object invariants, a particularly thorny programming challenge. An object invariant is a condition that describes the steady state of a program\u2019s data structures, something difficult to verify statically. Spec# addresses this concern by utilizing modular checking, in which the program is analyzed bit by bit, one piece at a time. By taking a look at each piece of a program, the whole can be verified.<\/p>\n

\u201cWe see that as a crucial thing in program development,\u201d Leino says. \u201cThe way we\u2019ve addressed it is that we have developed a number of rules. We call it the methodology, a discipline for how to program and how to write these object invariants. That was also one of the initial ideas that really got things started about how to undertake this project. We\u2019ve built lots of things on top of that since.\u201d<\/p>\n

Four years, obviously, is a long time to continue working on a single project. But Leino says it has been time well spent.<\/p>\n

\u201cEven though it has been one project,\u201d he says, \u201cthere are many different technical portions of it that have come in stages. There\u2019s some portion of it that we would want to explore in some way, so we explore that, and then we move on to the next part or maybe come back to some portion of it. Of course, as those years go on, the whole system becomes better, as well.<\/p>\n

\u201cFrom a research perspective, there are certainly lots of things still to explore. What we\u2019re trying to do is continue exploring in the context of Spec#, but we\u2019re also starting to apply similar techniques to verify C programs. I also have an interest in trying to do it with functional programs or dynamically typed programs. We\u2019re not at the stage where we say: \u2018Well, that was it. We\u2019re done.\u2019 There are many interesting things to usefully explore.\u201d<\/p>\n

Such as?<\/p>\n

\u201cSmoothing out the experience of using the system is a thing that we\u2019re working on,\u201d Leino replies. \u201cTrying to improve error messages or give more detail, and expanding the methodology to be able to handle more common programming idioms. Increasing the power of the specification language in certain ways. Improving the theorem-proving technology to make things faster and more effective.<\/p>\n

\u201cSome of the next steps that we\u2019re also involved in is trying to have an influence on the .NET Framework and other languages. Could we roll in the non-null types into the C# language? Having the contracts in the .NET library, in a way that tools can make use of it, is also something that we\u2019re working on actively with the people in that group.<\/p>\n

\u201cIf those things come together, then some of the current and next steps involve trying to take pieces of our technology from Spec# and trying to roll them into the Common Language Runtime, the .NET Framework, and languages like C#. We see Spec# as the research vehicle for exploring things, and the things that work out in a nice way we then hope to transfer into a product.\u201d<\/p>\n

Over the past few years, the project has benefited from the help of a number of colleagues, including Herman Venter, Francesco Logozzo, Peter M\u00fcller, and a succession of interns. It\u2019s clear that the passion for Spec# remains unabated.<\/p>\n

\u201cOne of the things that got me interested in the first place,\u201d he recalls, \u201cwas that, before I went back to graduate school, I worked at Microsoft as a programmer. I had great fun, and our group used contracts, and we found that we were able to have a much lower bug count than many other groups. Many of the errors we found were because of a broken contract.<\/p>\n

\u201cWhen I went back to graduate school, that interested me, to say, \u2018How can you take those specifications and check them statically?\u2019 That\u2019s a bit of what got me into this, and that still has me jazzed up, the idea that we could change the way programming is done. That vision, that such systems would be on every programmer\u2019s desktop in languages like Spec#\u2014that\u2019s certainly what\u2019s driving me.\u201d<\/p>\n","protected":false},"excerpt":{"rendered":"

By Rob Knies, Managing Editor, Microsoft Research Modern-day software development is notoriously challenging. Programs have become highly complex. Customer expectations have never been higher. Meeting quality standards is increasingly difficult. Challenging, yes. Difficult, perhaps. But such hurdles are not insurmountable, as Spec# demonstrates. Spec#, available for download, is a programming system devised by researchers from […]<\/p>\n","protected":false},"author":39507,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[],"msr_hide_image_in_river":0,"footnotes":""},"categories":[194488],"tags":[194493,215606,215603,193621,186580],"research-area":[13560],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-307580","post","type-post","status-publish","format-standard","hentry","category-program-languages-and-software-engineering","tag-net-framework","tag-high-quality-software","tag-programming-system","tag-software-development","tag-spec","msr-research-area-programming-languages-software-engineering","msr-locale-en_us"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[199565],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[],"msr_type":"Post","byline":"","formattedDate":"August 14, 2007","formattedExcerpt":"By Rob Knies, Managing Editor, Microsoft Research Modern-day software development is notoriously challenging. Programs have become highly complex. Customer expectations have never been higher. Meeting quality standards is increasingly difficult. Challenging, yes. Difficult, perhaps. But such hurdles are not insurmountable, as Spec# demonstrates. Spec#, available…","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/307580","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/39507"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=307580"}],"version-history":[{"count":2,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/307580\/revisions"}],"predecessor-version":[{"id":308648,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/307580\/revisions\/308648"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=307580"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=307580"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=307580"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=307580"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=307580"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=307580"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=307580"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=307580"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=307580"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=307580"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=307580"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}