.Net Contracts as Method Calls – Better Implementation and Adoption
Contracts in .Net are implemented as method calls (in the System.Diagnostics.Contracts namespace). This is in contrast to most of the other contracts-based tools that make use of other mechanisms to indicate contracts such as code comments in Java Modeling Language (JML), entity attributes or annotations in C4J, javadbc, and contract 1.4 Python (using annotations for function docstrings).
I think that representing contracts as method calls (in terms on an API) rather than annotations or comments is quite novel. Several advantages of using an API include :
Ease of extension– Constructs that can be used with attributes, annotations, and comments are limited and require a lot of effort in terms of parsing, extending compiler analyses including type checking and so on. IDE support is another facet with regard to the ease of extension; it is difficult to provide support for Intellisense when using attributes, annotations, and comments. IDE support is naturally available when authoring contracts as code.
Contract inheritance can be similarly supported out of the box, rather than by a separate treatment. (There would be another post on this).
Static contract checking of .Net contracts uses abstract interpretation (shown in less complicated way in this video. It’s pretty novel and to see how attributes-, annotations-, and comments- based contracts would fare in combination with abstract interpretation, I am going to make another post.)
Refactoring Support– Contracts as code become amenable to refactoring analyses like any other regular language entities. On the contrary, when having contracts as attributes, annotations, and comments, it is pretty difficult to adapt to refactorings and would require extension of parsing and compiler analyses.
Runtime Checking– To enforce contracts at runtime one has to include a binary rewriter in the build process when using attributes, annotations, and comments. Contracts as an API serve both as declarative contracts and as runtime-checked validation.
Extraction of Contracts– While attributes-, annotations-, and comments-based tools would need additional byte-code manipulation to extract contracts for contracts related tools this is included by default in the design of code contracts (Since compiling to MSIL (or any other intermediate language) is part of embedded contract languages design, see this paper.)
These positive points make code contracts much better than attributes-, annotations-, and comments- based contracts from implementation and adoption point of view.
Microsoft Research Projects of Interest – Contracts
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects to select for MSR researcher and post-doc positions.
Contracts
Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. They act as checked documentation of external and internal APIs. The contracts in the form of a library are used to improve testing via runtime checking, enable static contract verification, and documentation generation. The use of a library has the advantage that all .NET languages can immediately take advantage of contracts (See another post on this). There is no need to write a special parser or compiler. Furthermore, the respective language compilers naturally check the contracts for well-formedness (type checking and name resolution) and produce a compiled form of the contracts as MSIL.
Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.
Dafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. It is designed to support the static verification of programs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like algebraic datatypes, sets, and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code. The Dafny verifier itself is run as part of the compiler and is powered by Boogie and Z3.
Abstract State Machine Language (AsmL) is an executable specification language which can also be used with XML and MS-Word for literate programming. AsmL models operate at the level of .Net assembly and therefore work with all .Net languages. AsmL is usable via Spec Explorer, a model-based testing tool. AsmL enables testing that a system behaves as intended before it is programmed by means of a model. A model program in AsmL works by looking at the relevant states of the actual program and finding where the two do not conform.
Microsoft Research Projects of Interest – Spatial and Sociological Code Representations
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Spatial and Sociological Code Representations
Code Canvas houses editable forms of all of a projects documents and allows multiple layers of visualization over these documents. Developers often get interrupted from their work and when they return, they have to search/reorder all the concerned documents before beginning the actual work. The premise behind code canvas is that uniting the content and meta-content of a project onto a single surface it is possible to enable developers to leverage their spatial memory while coding. Other spatial projects include the use of spatial representations of development documents to allow developers to use spatial memory to find them.
Like spatial code representation, there are projects like Knowledge Flow that utilize sociological knowledge of a software development project — relation between the repositories (source code, bug database, etc.) and the engineers’ heads. Similarly, Codebook is a platfrom that uses a social networking-inspired approach to connect artifacts and people in software repositories. The premise behind these projects is that understanding the relation between actual code and what’s going on between the developers as they interact to develop a project can help in identifying how the project is taking shape. This will enable management to identify and affect better coordination and performance of developers.
Microsoft Research Projects of Interest – Testing
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Testing
Pex provides white box testing support for .Net apps. Pex can find input-output values of a method that can identify whether assertions about the base values are correct. Each contract acts as an oracle, giving a test run a pass/fail indication. Pex uses contracts to generate more meaningful unit tests by filtering out meaningless test arguments that don’t satisfy the pre-conditions. A nice Pex tutorial is here.
Moles is a lightweight framework for test stubs and detours in .NET that is based on delegates. Moles may be used to detour any .NET method, including non-virtual/static methods in sealed types. Moles is freely available on Visual Studio Gallery or bundled with Pex.
Automated Test Generation (ATG) attempts to provide support for automated testing using static and dynamic program analysis. It uses a combination of program analysis, testing, model checking and theorem proving described in this paper.
Microsoft Research Projects of Interest – Contracts
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Contracts
Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. They act as checked documentation of external and internal APIs. The contracts in the form of a library are used to improve testing via runtime checking, enable static contract verification, and documentation generation. The use of a library has the advantage that all .NET languages can immediately take advantage of contracts (See another post on this). There is no need to write a special parser or compiler. Furthermore, the respective language compilers naturally check the contracts for well-formedness (type checking and name resolution) and produce a compiled form of the contracts as MSIL.
Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants. Spec# comes with a sound programming methodology that permits specification and reasoning about object invariants even in the presence of callbacks and multi-threading. Spec# is a research vehicle that has been used to explore specifications and the dynamic/static tools that make use of them.
Dafny is an imperative object-based language with built-in specification constructs. The Dafny static program verifier can be used to verify the functional correctness of programs. It is designed to support the static verification of programs. The specifications include pre- and postconditions, frame specifications (read and write sets), and termination metrics. To further support specifications, the language also offers updatable ghost variables, recursive functions, and types like algebraic datatypes, sets, and sequences. Specifications and ghost constructs are used only during verification; the compiler omits them from the executable code. The Dafny verifier itself is run as part of the compiler and is powered by Boogie and Z3.
Abstract State Machine Language (AsmL) is an executable specification language which can also be used with XML and MS-Word for literate programming. AsmL models operate at the level of .Net assembly and therefore work with all .Net languages. AsmL is usable via Spec Explorer, a model-based testing tool. AsmL enables testing that a system behaves as intended before it is programmed by means of a model. A model program in AsmL works by looking at the relevant states of the actual program and finding where the two do not conform.
Microsoft Research Projects of Interest – Concurrency
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Concurrency
Chalice is an experimental language that explores specification and verification of concurrency in programs. The Chalice language supports dynamic object creation, dynamic thread creation (fork and join), mutual-exclusion and readers-writers locks, monitor invariants, thread pre- and postconditions. It allows fine-grained locking via specifications that track fractional permissions for memory locations. The research project also includes an automatic static program verifier for Chalice.
Poirot is a property checker for concurrent programs that uses language-independent techniques to efficiently search space of behaviors of a program for bugs. It works by first compiling the program in a supported language to a concurrent Boogie program. Next, it uses Corral, a symbolic exploration engine, to explore concurrent behaviors of the Boogie program looking for bugs. In case a bug is not found, Poirot produces a coverage report detailing the set of program behaviors that it covered.
The goal of tools for TLA+ specifications is to develop methods and tools that will permit engineers to apply formal specification and verification to high-level designs of concurrent algorithms and systems. The idea is to make the specification force a careful and rigorous examination of what an algorithm or system should do, separate from how it should do it and let the
verification catch bugs in an algorithm or a system design even before it is implemented, where one wants to catch and correct it.
Concurrent Revisions: Programming With Versioned Memory is a project that introduces a novel programming model for concurrent and/or parallel applications. It provides programmers with a simple, yet powerful and efficient mechanism (based on mutable snapshots and deterministic conflict resolution) to execute various application tasks in parallel even if those tasks
Microsoft Research Projects of Interest – Model Checking
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Model Checking
The Zing project aims at a flexible and scalable systematic state space exploration infrastructure. It uses high-level models that may involve reasoning with rich background universes or combinations of different theories, that arise in various practical applications.
Z3 is a high-performance theorem prover that supports linear real and integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated with a number of program analysis, testing, and verification tools from Microsoft Research. These include: Spec#/Boogie, Pex, Yogi, Vigilante, SLAM, F7, VS3, FORMULA, and HAVOC. It can read problems in SMT-LIB and Simplify formats.
Microsoft Research Projects of Interest – Verification and Property Checking
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Verification and Property Checking
Boogie is an intermediate verification language that can be used to build program verifiers.
F7 is an enhanced typechecker for the F# programming language. F7 is based on the premise that it should be possible to check various security properties of F# implementation code by typing.
The project End-to-end Security Verification using Refinement Types is concerned with building, verifying, and deploying systems with provable security guarantees using refinement and affine types to verify programs written in a core subset of F#.
Yogi is a research project about software property checking that combines static analysis with testing.
Microsoft Research Projects of Interest – Analysis
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Analysis
ExtendedReflection is Dynamic Analysis Framework for .NET that takes care of instrumenting MSIL bodies at runtime and exposes more than 200 .NET callbacks, such as method enter/exit, argument values or field writes. It also enables redirection of arbitrary method calls. With ExtendedReflection, it is possible to write dynamic analysis tools in any .NET language, without having to understand the low-level CLR internals.
Holmes is a statistical test tool that automatically finds the most likely cause of test failures by analyzing fine-grained path coverage data and identifying code paths that strongly correlate with failures.
Microsoft Research Projects of Interest – Types
Microsoft has a number of great groups at the MSR and a lot of interesting projects. I am nearly done with my PhD and am looking for possible opportunities at various research labs and groups. In this series of posts, I am going to briefly summarize interesting projects select for MSR researcher and post-doc positions.
Types
Dminor is a first-order functional language based on refinement type and type-tests. It is purported to handle many dynamic tests statically.
Typed Assembly Language for Object-Oriented Compilers project uses typed intermediate languages and Typed Assembly Languages (TAL) (type annotated native code) to guarantee safety properties of native code.
Sagar Sunkle's Blog 