When demoing the CodeContracts static checker, often people ask me what’s underneath. I tell them that is based on abstract interpretation, a theory developed in the late 70s by two French computer scientists, Patrick and Radhia Cousot. According to abstract interpretation, concrete program executions can be observed at different abstraction levels (called abstract semantics). A…

## Inter-procedural inference of conditions to error in cccheck

Today we pushed out a new release of CodeContracts. Among the many improvements, bug fixes, etc. we improved the inference of pre-conditions to errors. The static checker now also provides inter-procedural error traces. But how it works? Let me illustrate the inference of preconditions with this example private int Max(int[] a){ var max = a[0];…

## How to prove properties of finite state machines with cccheck

In the previous post we saw how to use cccheck to prove that we did not forgot any case in a switch statement. Some friend in Microsoft product groups asked if we can do more. For instance, if we can prove properties about a finite state machine using the CodeContracts static checker. The answer is…

## How to use cccheck to prove no case is forgotten

Today we use the CodeContracts static checker to prove that no case is missing in a switch statement. This post is inspired by some feedback we had from CodeContracts users in product groups. The problem. Suppose that we want to write a program to cook pasta. Cooking pasta is a simple. First we let the…

## FAQ #1: What is the difference between Assert and Assume?

In CodeContracts, as in most verification systems, we have two APIs to check the validity of an expression at a given program point: Contract.Assert and Contract.Assume. People (even very smart Academics with a Ph.D. in computer science!) often get confused by the two concepts. They tend to use Contract.Assert most of the times. In this first…

## Welcome to my blog!

Hello. I’ve decided to start a blog to help CodeContracts users, present some tricks to get the best from the tools, in particular the static checker and in general to give some update on what’s new and cool in the program analysis and verification environments as well as to explain some of the theory and…