Language-Agnostic Specification and Verification Invited Talk

摘要

Over the last few years we have been working on bringing simple and pragmatic program specification and verification to programming languages targeting the Microsoft .NET platform. In this talk I will discuss the motivation and trade-offs influencing our design. The specifications and static verification are targeted at the general developer, not the verification enthusiast. It is thus important to us to use a single form of specifications that meets three simultaneous goals:rn1. Specifications serve as documentation. They must be as readable as possible.rn2. Specifications should be executable. This motivates writing specifications for testing and immediate perceived benefit, without consideration of static verification.rn3. Specifications should be usable in static verification.rnOur specification approach is language-agnostic in that we use idiomatic code written in the developer's source language to express preconditions and postconditions. Preconditions and postcondi-rntions are expressed as calls to the static methods Contract. Requires and Contract. Ensures. Special dummy methods are used to refer to the method result value as well as referring to the old value of an expression, meaning the value of the expression on method entry. The conditions in the example in Figure 1 are written in C# expression syntax. The same specification written in Visual Basic is shown in Figure 2.rnSuch a language-agnostic approach has numerous advantages:rn1. The developer need not learn a new language for writing specifications. Predicates are boolean conditions expressed in the source language.rn2. No new front-ends or compilers need to be written or used. The original language compilers are used to compile the contractsrninto .NET intermediate language (MSIL). As a side-effect, the compilers check the syntax and types, thus avoiding errors in specifications, such as unresolved names etc, that would arise if the specifications were written in comments or attributes.rn3. The source language development environment helps writing specifications in that it provides all the features to specification writing it already provides for code writing such as highlighting, intellisense, completion, etc.rn4. The generated intermediate code for the conditions has a fixed interpretation provided by MSIL. No new semantics for the specifications needs to be defined. Furthermore, the compiled code acts as a persisted format of specifications consumable by a variety of tools.rnThe language independence extends from the specification language to the verification tool itself since the verification is performed on the generated MSIL rather than on the source.rnDue to our target audience, it is also important that the static verification is highly automated. In particular, we wish to avoid the need for programmer written loop invariants whenever possible. As a result, rather than building our verifier on standard techniques such as proof obligation generation discharged by an SMT solver, our verifier is based on abstract interpretation. It thus computes loop invariants and strongest postconditions automatically for a variety of abstract domains.rnAlthough we use modular verification that in principle requires specifications at all method boundaries, we use techniques to infer pre- and postconditions whenever possible.