A light-weight approach to applying formal methods in software development
Xiaoping Jia, Sotirios C. Skevoulis · 1999
In recent years extensive research effort has been made in the area of formal methods with remarkable results. This effort though, did not have much practical impact in the sense of acceptance within the software development industry. The reason for such a misfortune can be found in certain constraints and burdens that have been imposed by the promise, coming from the formal methods research community, that the use of formalization could bring absolute correctness in designs and implementations. If we allow formal methods to aim at more modest goals than absolute correctness and absence of errors, then we may be able to apply it at a relatively low cost in mainstream software industry. The detection of common programming errors is definitely such a goal. We provide a practical mechanism to assist the application of formal methods in specific areas of software development such as the detection of common potential errors in programs at compile time. Specifically, we present a generic approach to statically analyzing Java programs in order to detect potential errors. It is based on the concept of class invariant and includes two main generic algorithms to determine a class invariant and detect a potential violation. Each one of those algorithms is complemented with a number of specialized algorithms that carry out specific analysis depending on the kind of error under investigation. For a Java class, invariants related to the category of error under examination are automatically generated and used to assess the validity of variable usage in the implementation of this class. Our solution is theorem proving based and surpasses the capabilities of existing approaches in detection of coding errors. The theorem prover has been tailored with specific automated tactics and decision procedures to discharge proof obligations with no user guidance. In fact, the proving component is completely transparent to the user. Our research effort is experimental in nature. Its success can be judged through experiments rather than theoretical proofs and analyses. Experimentation is used as a feedback mechanism to our theoretical studies and solutions. The goal is to gain and demonstrate effectiveness, through experimentation.