Logic program comparison method for verifying a computer program in relation to a system specification

• US 5,481,717 A
• Filed: 04/12/1994
• Issued: 01/02/1996
• Est. Priority Date: 04/12/1993
• Status: Expired due to Fees

• Current Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Original Assignee: Kabushiki Kaisha Toshiba (Toshiba Corporation)
• Inventors: Gaboury, Pierre
• Primary Examiner(s): Kriess, Kevin A.
• Application Number:
  US08/229,427
• Time in Patent Office: 630 Days
• Field of Search: 395/700, 395/650
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 30/3323 using formal methods, e.g. equivalence checking or property checking

Abstract

It is an object of the present invention to provide a logic program comparison method which makes it possible to do verification by comparing parameterized logic programs and which increases the efficiency of the verification. The keyboard 1 and the input section 4 read two logic programs. The conversion section 5 converts the logic programs into the first and second finite state machine descriptions. The comparison section 6 determines whether there exists an equivalence between the states, between input values, and between output values of the first and second descriptions, and determines whether both descriptions produce respective outputs values deemed equal for all respective inputs deemed equal, for all respective states deemed equal. The result of the comparison is output through the output section 7 and the display unit 2.

Claims

1. A computer-based logic program verification method comprising:

receiving two logic programs, each having procedures with program variables, each of said program variables being of a corresponding data type;

converting said logic programs to a first and second finite state machine description respectively, each having internal states, input values and output values, comprising,

determining the data types of variables of said logic programs,

converting said programs to a completed form having expressions in disjunctive form,

expanding procedure calls within said programs into corresponding procedure bodies,

translating said programs into corresponding transition functions composed of transition function expressions;

determining from said transition functions whether there exists an equivalence between internal states, between input values, and between output values of said first and second finite state machine descriptions, and determining whether said finite state machine descriptions produce respective output values deemed equal for all respective inputs deemed equal and for all respective states deemed equal; and

outputting the result of said comparing step.

2. A computer-based logic program verification method according to claim 1, wherein said receiving step receives generic queries as part of said programs and wherein said converting step performs said converting based on said generic queries.

3. A computer-based logic program verification method according to claim 1, wherein said converting step determines said data types by applying static analysis to said programs.

4. A computer-based logic program verification method according to claim 1, wherein said comparing step uses a constraint solving technique comprising the steps of:

associating a unique constraint variable with each program variable denoting an input, output, or state variable;

grouping each constraint variable of a particular data type from said first logic program with every other constraint variable of a corresponding data type from said first logic program to form pairs;

grouping each constraint variable of a particular data type from said second logic program with every other constraint variable of a corresponding data type from said second logic program to form pairs;

generating a conjunction of inequalities between each pair of said constraint variables;

generating, for all possible reorderings of the expressions in disjunctive form equalities between constraint variables occurring in respective positions;

taking the conjunction of inequalities and said generated equalities as constraints to a new expression;

solving the new expression using the constraints.

5. A computer-based logic program verification method according to claim 1, wherein said logic programs are described by definite clauses that are a subset of predicate logic, and wherein a definite clause is restricted to one of a query, a rule and a fact.

6. A computer-based logic program verification method according to claim 1, wherein recursive procedures having recursive procedure bodies are mapped into FSMs by mapping the recursive procedure bodies into corresponding iterative expressions, thus removing corresponding recursive calls.

7. A logic program verification method according to claim 1, wherein said converting step further comprises:

permuting the transition function expressions to group together variables with common values, and

replacing each variable by a unique code;

permuting the transition function expressions to group together variables with common values;

converting transition function expressions where one of said internal states takes on multiple values into multiple expressions wherein said one of said internal states takes on a different corresponding value in each of said multiple expressions;

encoding each transition function expression having a unique internal state with a unique code.