An Automatic Approach to Generating a State Diagram from a Contract-Based Class

Stale diagrams are commonly used to describe the dynamic behavior of an individual object. In other words, stale diagrams can represent sequences of operations in classes. fit addition, slate diagrams are commonly used for various purposes: test case generation, formal verification and code generation. Because stale diagrams describe all the possible dynamic behaviors of an object, it is very difficult to draw and understand them. This paper presents an automated approach to the generation of a stale diagram from a contract-based class. That is, a state diagrams are automatically generated by analyzing pre/post conditions of each operation. We also developed a tool for supporting our approach and applied the tool to two case studies, MicrowaveOven and BlankReader. We have found that the proposed technique and tool can be useful for constructing state diagrams from contract-based classes.