Identifying Candidate Invariant Conditions of Running Program

T.E. Setiadi, K. Nakayama, Y. Kobayashi, and M. Maekawa (Japan)


Invariant condition, program execution, and Aspect Oriented Programming (AOP).


The increasing size and complexity of software products often make software engineers use already built components. By using those components, software engineers need to understand the components usage and their behavior. Unfortunately, good documentation might not always be available. Knowing some program invariant can help software engineers in understanding component behavior. This paper describes a Java Invariant Analyzer (Javian), a tool that helps identifying candidate invariant conditions of a running Java program. Javian reports candidate invariant conditions by analyzing the program execution using some clues from the source code. It can also find the location that satisfies a given condition. The output from this system can be used to help in writing partial specification for the program that possibly can be used as the input for the verification system.

Important Links:

Go Back