The Spec# Programming System: An Overview

Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte

Abstract

The Spec# programming system is a new attempt at a more cost effective way to develop and maintain high-quality software. This paper describes the goals and architecture of the Spec# programming system, consisting of the object-oriented Spec# programming language, the Spec# compiler, and the Boogie static program verifier. The language includes constructs for writing specifications that capture programmer intentions about how methods and data are to be used, the compiler emits run-time checks to enforce these specifications, and the verifier can check the consistency between a program and its specifications.

Details

Publication typeInproceedings
Published inCASSIS 2004, Construction and Analysis of Safe, Secure and Interoperable Smart devices
Pages49-69
Volume3362
SeriesLecture Notes in Computer Science
PublisherSpringer
> Publications > The Spec# Programming System: An Overview