Dynamically Michael Discovering Likely Program to Support Program Evolution D Ernst Jake CockrelIt William Dept of Computer Science Engineering University of Washington Box 352350 Seattle WA 98195 2350 USA l 206 543 1695 mernst jake notkin cs washington edu G Griswoldt Invariants and David Notkint Dept of Computer Science Engineering University of California San Diego 0114 La Jolla CA 92093 0114 USA l 619 534 6898 wggOcs ucsd edu variable values from which we then infer invariants As with other dynamic approaches such as testing and profiling the accuracy of the inferred invariants depends on the quality and completeness of the test cases additional test cases might provide new data from which more accurate invariants can be inferred This approach is complementary to static approaches which examine the program text but do not run the program ABSTRACT Explicitly stated program invariants can help programmers by identifying program properties that must be preserved when modifying code In practice however these invariants are usually implicit An alternative to expecting programmers to fully annotate code with invariants is to automatically infer invariants from the program itself This research focuses on dynamic techniques for discovering invariants from execution traces This paper presents two initial experiences with a set of techniques and invariants from execution This paper reports two results First it describes techniques for dynamically discovering invariants along with an instrumenter and an inference engine that embody these techniques Second it reports on the application of the engine to two sets of target programs In programs from Gries s work on program derivation we rediscovered predefined invariants In a C program lacking explicit invariants we discovered invariants that assisted a software evolution task related results stemming from our this approach Our first result is an implementation for discovering traces Section 3 Our second result is the application of our inference engine to two sets of target programs The first set of programs GriBl was derived taken from The Science of Programming from formal preconditions postconditions and loop invariants Given runs of the program over randomly generated inputs our techniques discover those same program properties plus some additional ones Section 2 The second set of programs C programs originally from Siemens HFG094 and modified by Rothermel and Harrold RH98 is not annotated with invariants nor is there any indication that invariants were used in their construction Section 4 shows how numeric invariants dynamically inferred from one of these programs assisted in understanding and changing it Keywords Program invariants formal specification software evolution dynamic analysis execution traces logical inference pattern recognition 1 INTRODUCTION Invariants play a central role in program development Representative uses include refining a specification into a correct program static verification of invariants such as type declarations and runtime checking of invariants encoded as assert statements Section 5 presents performance measurements and discusses techniques for mitigating combinatorial blowups and otherwise improving runtime performance Section 6 surveys related work and Section 7 concludes Invariants play an equally critical role in software evolution In particular invariants can protect a programmer from making changes that inadvertently violate assumptions upon which the program s correct behavior depends The near absence of explicit invariants in existing programs makes it all too easy for programmers to introduce errors while making changes 2 REDISCOVERY OF INVARIANTS To introduce our approach and illustrate the output of our tool we present the invariants detected in a simple program taken from The Science of Program ming Gri81 a book that espouses deriving programs from specifications Unlike typical programs for which it may be difficult to determine the desired output of invariant detection many of the book s programs include preconditions postconditions and loop invariants that embody important properties of the computation Our invariant detector successfully reports all the formally specified preconditions postconditions and loop invariants in chapters 14 and 15 of the book chapter 14 is the first in which such programs appear An alternative to expecting programmers to annotate code with invariants is to automatically infer invariants In this research we focus on the dynamic discovery of invariants we execute a program on a collection of inputs and extract Permission to m e digital or hard topics of all or part orthis work co1 personalor classroom USCis granted without fee provided that COPiCs As a simple example consider a program that sums the elements of an array Figure 1 We transliterated this program to a dialect of Lisp enhanced with Gries style control are ot In or distributed for profit or commercial advantage and that copies hear this notice and the full citation 011the first page To WJY other visc to republish to post on servers nr to rcdistrihute to lists requires prior specific permission and or B t w ICSE 9 Los Angcks C A Copyright ACM 1999 l 581 13 074 0 99 05 00 213 i s 0 o doi n i 9 i 1 s b i od Precondition n 2 0 Postcondition s c j 0 5 j II bL Loop invariant 0 2 i 5 n and s cj 0 5 j i bb Figure 1 Gries program 15 1 1 Gri81 p 1801 and its formal specification The program sums the values in array b of length n into result variable s The statement i s 0 O is a parallel simultaneous assignment of the values on the right hand side of the to the variables on the left hand side The do od form repeatedly evaluates the condition on the left hand side of the and if it is true evaluates the body on the right hand side the form terminates when the condition evaluates to false inserted at the beginning of the program at the loop program in which 100 to head and at the end of the program We ran this on 100 randomly generated arrays of length 7 to 13 each element was a random number in the range 100 inclusive Figure 2 shows the output of our invariant detector given the data trace file The precondition BEGIN inferences record the relationship between N and the length of array B which is crucial to the correctness of the program but omitted from the formal invariants the range of values for N appearing in the test cases and that the test case array elements were always at least 100 several others 100