Specification and verification: the Spec# experience

摘要: Spec# is a programming system that puts specifications in the hands of programmers and includes tools use them. The an object-oriented language with specification constructs, compiler emits executable code run-time checks for specifications, methodology gives rules structuring programs using static program verifier attempts to mathematically prove correctness programs. This paper reflects on six-year experience building Spec#, scientific contributions project, remaining challenges seek establish correctness, prospects incorporating verification into everyday software engineering. 0. INTRODUCTION: THE SPEC# VISION Software engineering process authoring fulfill some worldly needs. It expensive endeavor provides difficulties at all levels. At top level, gathering requirements usually exploratory iterative process. Any change ripples through parts artifact further complicated by having maintain previous versions software. level itself, interaction between modules requires understanding what expected can be assumed interacting modules. each module, one problem consistency data structures, let alone remember it means particular structure consistent. individual operations, algorithmic details tricky get right. Two common themes among these are useful accurate documentation making sure adhere documented behavior do not misuse features language. (pronounced “speck sharp”) research project aimed addressing two problems. To combat first problem, takes well-known approach providing contracts, constructs document behavior. second adds automatic Permission make digital or hard copies part this work personal classroom granted without fee provided made distributed profit commercial advantage bear notice full citation page. copy otherwise, republish, post servers redistribute lists, prior specific permission and/or fee. Copyright 2009 Barnett, Fahndrich, Leino, Muller, Schulte, Venter. tool support, which verifier. set out explore programmer time receiving benefit from support intended just help ensure but also, importantly, lure recording their design decisions knowing will rot as stale comments. In paper, we describe system, along our initial goals have done it, how has already had impact, now, retrospect, view decisions. 1. SONGS OF INNOCENCE We started 2003 attempt build comprehensive [4]. Our dream was real verification—a “the masses” could work. wanted push boundaries technology closer realizing aspirations. Let us consider more detail lay land project. Program several decades old, starting formal underpinnings semantics techniques proving [13]. Supported mechanical proof assistants, early verifiers were GYPSY Boyer-Moore prover [0] Stanford Pascal Verifier [18]. Later systems, still used today, include full-featured assistants like PVS [23] Isabelle/HOL [22]. Another uses extended checkers ESC/Modula-3 [9] ESC/Java [12]. These been closely integrated existing languages value automation over expressivity mathematical guarantees finding errors program. enabled breed combined decision procedures today known Satisfiability Modulo Theories (SMT) solvers [8]. them easier cost-effective use, intentionally designed unsound, is, they may miss certain errors. Dynamic checking always Eiffel [20], also pioneered inclusion suite Java Modeling Language (JML) [16] included facility dynamic [5]. influenced JML, strong influence both