Method, program, and system for specification verification

• US 9,208,151 B2
• Filed: 10/24/2012
• Issued: 12/08/2015
• Est. Priority Date: 10/25/2011
• Status: Expired due to Fees

• Current Assignee: International Business Machines Corporation
• Original Assignee: International Business Machines Corporation
• Inventors: Kawachiya, Kiyokuni, Tatsubori, Michiaki
• Primary Examiner(s): Somers, Marc
• Application Number:
  US13/658,884
• Publication Number:
  US 20130103652A1
• Time in Patent Office: 1,140 Days
• US Class Current: 1/1
• CPC Class Codes: G06F 16/93 Document management systems

Abstract

A method, program, and system for specification verification. The method includes the steps of: (a) retaining a plurality of documents as groups of abstract documents that display values capable of indicating each metadata; (b) separating the group of abstract documents based on an input condition of an operation; (c) adding a new abstract document by using, based on an output condition, at least one the operation within a group of the operations; (d) separating the abstract documents according to overlapping ranges designated by the metadata; (e) unifying the abstract documents according to overlapping ranges designated by the metadata; (f) repeating the steps (b) to (e) until a termination condition is satisfied; and (g) verifying whether an incomplete abstract document exists when the termination condition is satisfied.

Claims

1. A method for verifying a specification, comprising the steps of:

(a) retaining, by a processor of a computer system, a plurality of abstract documents, each said abstract document of said plurality indicating a value corresponding to a metadata of that document;

(b) separating, by the processor, a group of abstract documents based on an input condition of an operation;

(c) adding, by the processor, a new abstract document to said group by using, based on an output condition, at least one said operation within a group of said operations;

(d) separating, by the processor, said abstract documents according to overlapping ranges of values designated by each said metadata of abstract documents indicated in said group;

(e) unifying, by the processor, said abstract documents according to overlapping ranges of values designated by each said metadata of abstract documents indicated in said group;

(f) repeating said steps (b) to (e) until a termination condition is satisfied; and

(g) verifying, by the processor, whether an incomplete abstract document exists when said termination condition is satisfied;

wherein said plurality of abstract documents associated with a plurality of said metadata are processed;

wherein said group of said operations are applied collectively by an operation specification specifying document processing operations;

wherein said input condition that is a condition of a range of values of said metadata capable of application of a respective operation is retained for each of said operation; and

wherein an output condition that is a change of said metadata value after use of said respective operation is retained for each of said operation.

2. The method according to claim 1, further comprising the step of:

forming a graph structure by forming nodes from said abstract documents and links from said operations and retaining said abstract documents.

3. The method according to claim 2,

wherein said termination condition comprises detecting that said abstract documents have not been changed by said applied operations.

4. The method according to claim 3, further comprising the step of:

repeating said use of said operations at least one time before said step of verifying, in response to detection of non-occurrence of change of said abstract documents by said applied operations.

5. The method according to claim 2,

wherein said operation specification comprises a completion condition described by a specific state of said metadata;

and

wherein said step of verifying further comprises the steps of;

applying a completion mark, among said abstract documents that satisfy said completion condition, to reverse abstract documents that arrived at said graph structure in reverse order; and

determining verification failure if said reverse abstract document is without an applied completion mark.

6. The method according to claim 5, further comprising the step of:

presenting, among initial abstract documents, a path going up to said abstract document without said applied completion mark as a failure example.

7. A computer readable product comprising a non-transitory storage medium tangibly embodying a computer readable program code having computer readable instructions which when implemented, cause a computer to carry out the steps of a method comprising:

(a) retaining, by a processor of a computer system, a plurality of abstract documents, each said abstract document of said plurality indicating a value corresponding to a metadata of that document;

(b) separating, by the processor, a group of abstract documents based on an input condition of an operation;

(c) adding, by the processor, a new abstract document by using, based on an output condition, at least one said operation within a group of operations;

(d) separating, by the processor, said abstract documents according to overlapping ranges of values designated by each said metadata of abstract documents indicated in said group;

(e) unifying, by the processor, said abstract documents according to overlapping ranges of values designated by each said metadata of abstract documents indicated in said group;

(f) repeating said steps (b) to (e) until a termination condition is satisfied; and

(g) verifying, by the processor, whether an incomplete abstract document exists when said termination condition is satisfied;

wherein said plurality of abstract documents associated with a plurality of said metadata are processed;

wherein said group of said operations are applied collectively by an operation specification specifying document processing operations;

wherein said input condition that is a condition of a range of values of said metadata capable of application of a respective operation is retained for each of said operation; and

wherein an output condition that is a change of said metadata value after use of said respective operation is retained for each of said operation.

8. The computer readable storage medium according to claim 7, further comprising the step of:

forming a graph structure by forming nodes from said abstract documents and links from said operations and retaining said abstract documents.

9. The computer readable storage medium according to claim 7,

wherein said termination condition comprises detecting that said abstract documents have not been changed by said applied operations.

10. The computer readable storage medium according to claim 9, further comprising the step of:

repeating said use of said operations at least one time before said step of verifying, in response to detection of non-occurrence of change of said abstract documents by said applied operations.

11. The computer readable storage medium according to claim 8,

wherein said operation specification comprises a completion condition described by a specific state of said metadata;

and

wherein said step of verifying further comprises the steps of;

applying a completion mark, among said abstract documents that satisfy said completion condition, to reverse abstract documents that arrived at said graph structure in reverse order; and

determining verification failure if said reverse abstract document is without an applied completion mark.

12. The computer readable storage medium according to claim 11, further comprising the step of:

presenting, among initial abstract documents, a path going up to said abstract document without said applied completion mark as a failure example.

13. A specification verification system, comprising:

a processor device configured to;

(a) retain a plurality of abstract documents, each said abstract document of said plurality indicating a value corresponding to a metadata of that document;

(b) separate a group of abstract documents based on an input condition of an operation;

(c) add a new abstract document to the separated group by using, based on an output condition, at least one said operation within a group of said operations;

(d) separate said abstract documents according to overlapping ranges of values designated by each said metadata of abstract documents indicated in said group;

(e) unify said group of abstract documents according to overlapping ranges designated by each said metadata of abstract documents indicated in said group;

(f) repeat functions (b) to (e) until a termination condition is satisfied; and

(g) verify whether an incomplete abstract document exists when said termination condition is satisfied;

wherein said plurality of abstract documents associated with a plurality of said metadata are processed;

wherein said group of said operations are applied collectively by an operation specification specifying document processing operations;

wherein said input condition that is a condition of a range of values of said metadata capable of application of a respective operation is retained for each of said operation; and

wherein an output condition that is a change of said metadata value after use of said respective operation is retained for each of said operation.

14. The system according to claim 13, wherein said processor device is further configured to:

form a graph structure by forming nodes from said abstract documents and links from said operations and retaining said abstract documents.

15. The system according to claim 13,

wherein said termination condition comprises detecting that said abstract documents have not been changed by said applied operations.

16. The system according to claim 15, wherein said processor device is further configured to:

repeat said use of said operations at least one time before said verification of whether said incomplete abstract document exists, in response to detection of non-occurrence of change of said abstract documents by said applied operations.

17. The system according to claim 14,

wherein said operation specification comprises a completion condition described by a specific state of said metadata;

and

wherein said processor device is further configured to;

apply a completion mark, among said abstract documents that satisfy said completion condition, to reverse abstract documents that arrived at said graph structure in reverse order; and

determine verification failure if said reverse abstract document is without an applied completion mark.

18. The system according to claim 17, wherein said processor device is further configured to:

present, among initial abstract documents, a path going up to said abstract document without said applied completion mark as a failure example.