A Start

This blog talks about verifiable software. Here I post my thoughts on how this can be achieved, how to write a verifying compiler and what requirements must be made on the language to write code which is verifiable.

The basic requirements for a verifiable language and a verifying compiler:

– The language must allow to write highly efficient code. It should include the possibility to write functional and/or imperative code. Object orientation should be supported.

– The language must allow the software developer to express certain properties at certain points of the computation (called assertions) in order to specify what a certain part of the software has to achieve.

– The assertion language must be natural to the developer and expressive enough.

– The software developer should not be forced to supply proofs in detail, only to give proof outlines (or just to state the assertions).

– The compiler should be able to prove the asssertions of the developer or give enough information to the programmer so that he/she can fix the problem.

– Concurrency should be integral part of the language. It should be possible to statically verify liveness conditions (deadlock free, divergence free).

– The language should be scalable to allow to write very small and very large programs.

– The verifier must work in a modular way, i.e. apply only local reasoning to verify the software.

No currently available language satisfies these requirements. The closest ones are Spec# and Eiffel because they allow to express assertions. Scala is a candidate as well, because it combines functional and imperative programming very well (but it lacks assertions).

I will start with a modified version of Eiffel (so called Modern Eiffel). However the techniques shall be applicable to any other language which can be made strict enough and expressive enough.

Advertisements
  1. #1 by the Jaywalker on September 16, 2011 - 10:09 am

    Why not Java and JML? To attract mainstream developers towards verification of software, one has to focus on the languages they use. Almost all verification attempts are by people focusing on functional programming languages, perhaps due to the immutable nature of data in there?

    • #2 by helmutbrandl on September 19, 2011 - 12:24 pm

      As I said in my post: Any language expressive and rigid enough can be used to verify SW. I have chosen Eiffel, because it already has many needed elements (e.g. assertions integrated into the language, command query separation). Since I can work only a limited amount of my time on that subject I had to choose a language which is close to the needs.

      But I agree with your point. Mainstream languages like C++, java would be better to address a wider audience. I assume when the concepts are mature enough, any language (C++, java, C#) can be modified to achieve the same goal. But I am sure it must be modified in many areas. Therefore a verifiable java will look different to standard java.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: