Using multiple graphs of programs to modify specifications

The paper presents a supporting technique for changing specification documents automatically so that the specifications can be consistent with source codes when the source codes are modified. In our technique, we represent a program with multiple graphs and we consider the changes on programs as the modification of the graphs. The modification of the graphs is formalized with a sequence of the operation on the graphs. We design the rules of how to relate the operations on program graphs to the operations on graphs that represent specification documents. By applying these rules, we can detect what modification and which parts of the specification document should be made to maintain the consistency between the specification and the program, when the program is modified