Process and system for developing mathematically validated object-oriented software

• US 6,959,432 B2
• Filed: 03/05/2002
• Issued: 10/25/2005
• Est. Priority Date: 03/08/2001
• Status: Expired due to Fees

• Current Assignee: Escher Technologies Limited
• Original Assignee: Escher Technologies Limited
• Inventors: Crocker, David
• Primary Examiner(s): DAS, CHAMELI
• Application Number:
  US10/091,122
• Publication Number:
  US 20020162091A1
• Time in Patent Office: 1,330 Days
• Field of Search: 717/126, 717/116, 717/127, 717/131, 717/121, 717/120, 717/106, 717/108, 717/130, 719/316, 719/315, 714/38, 716/1
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3466 Performance evaluation by tracing or monitoring
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013
• CPC Class Codes: G06F 8/10 Requirements analysis; Specification techniques

Abstract

A process and a system are used to verify that an object-oriented software component described in an extended programming language behaves correctly with respect to an abstract data model and specifications of the operations that may be performed on it The process and system also verify for an assembly of components that whenever an operation on a component is invoked, the correct conditions specified for that operation and component exist, and that specified properties hold for a component of the assembly.

Claims

1. A computer implemented process for developing mathematically validated object oriented software comprising the steps of:

a) writing an abstract specification of a class, methods and expected properties of a component of the software, wherein the abstract specification of the methods includes a two-part postcondition such that when one of the methods is overridden by an overriding method in a descendent class one part of the one of the methods is inherited and another part the one of the methods is not inherited by the overriding method;

b) checking the abstract specification for errors and verifying that the class has the expected properties;

c) generating executable code for the class from the abstract specification;

d) running and evaluating the executable code to check that the code meets requirements other than a required speed of performance; and

e) evaluating the speed of performance when handling data sets commensurate to a size of data sets of the software component is required to handle.

2. A process as claimed in claim 1, wherein step c) of generating executable code includes the further step, where the specification is too complex to generate executable code directly, of refining the method by specifying a series of operations to be undertaken, to produce a refined method and verifying that the refined method behaves in accordance with the abstract specification before generating executable code.

3. A process as claimed in claim 2, wherein the step of refining the method includes providing an algorithm of program statements including postcondition statements.

4. A process as claimed in claim 1, wherein step d) of running and evaluating the executable code, includes the further step, where the code does not meet requirements, of identifying the defects and correcting the abstract specification and then repeating the process from step b).

5. A process as claimed in claim 1, wherein the step e) of evaluating the speed of performance, includes the further steps, where the speed of performance is inadequate, restructuring data maintained by the class, adding variable declarations for the restructured data, and refining the methods and constructors to take account of the restructured data and generating executable code.

6. A process as claimed in claim 1, wherein the step e) of evaluating the speed of performance, includes the further steps, where the speed of performance is inadequate, of refining the method to produce a refined method and verifying that the refined method meets the specifications of original method, and generating executable code.

7. A process as claimed in claim 1, wherein the abstract specification includes a name of the class, a list of other class or classes and/or interfaces that said class inherits from, an abstract model of data maintained by the class, abstract specifications of the methods and constructors of the class, and theorems of expected behaviour of the class and the methods and constructors.

8. A process as claimed in claim 7, wherein the abstract model of data includes declarations of abstract variables and may optionally include class invariants which are conditions concerning values of the abstract variables that are expected always to be true and declarations of abstract methods private to the class that assist in defining the class invariants and what other methods achieve.

9. A process as claimed in claim 7, wherein the abstract specifications of the methods and constructors of the class include:

a method name;

a method parameter list; and

a definition of what the method achieves.

10. A process as claimed in claim 9, wherein the abstract specifications of the methods and constructors of the class further include one or more of a method result type, a precondition that is required to hold whenever the method is called;

and a post-assertion description of conditions expected to hold when the method returns.

11. A process as claimed in claim 7, wherein a description of the class is divided into regions:

an abstract region containing the abstract data model and also private methods and constructors referred to elsewhere in specifications of the class;

an internal region containing re-implemented data and redundant data and also private methods and constructors referred to in re-implementations of other methods;

a confined region of methods and constructors that are used only within the class and within other classes that inherit from that class; and

an interface region of methods and constructors accessible to any program or components that use instances of the class.

12. A process as claimed in claim 1, wherein the step c) of generating executable code includes the steps of:

i) tokenizing the abstract specification to form a token stream and building a representation of the abstract specification;

ii) passing the token stream;

iii) binding identifiers and operators to declarations;

iv) converting the specifications contained therein to standard forms;

v) generating a new instance of each variable at every point at which the variable is changed, effectively replacing each variable by a succession of constants;

vi) generating proof obligations to represent requirements for program correctness;

vii) proving the obligations;

viii) using the abstract specification to generate a test harness or a set of test data for testing speed of performance;

ix) generating code statements to implement the specification where no code is provided;

x) translating the code statements to easily translatable form; and

xi) translating easily translatable form to an output language.

13. A system for developing mathematically validated object oriented software comprising:

a) means for writing an abstract specification of a class, methods and expected properties of a component of the software, wherein the abstract specification of the methods includes a two-part postcondition such that when one of the methods is overridden by an overriding method in a descendent class one part of the one of the methods is inherited and another part the one of the methods is not inherited by the overriding method;

b) means for checking the abstract specification for errors and verifying that the class has the expected properties;

c) means for generating executable code for the class from the abstract specification;

d) means for running and evaluating the executable code to check that the code meets requirements other than a required speed of performance; and

e) means for evaluating the speed of performance when handling data sets commensurate to a size of data sets of the software component is required to handle.

14. A system as claimed in claim 13, wherein the means for generating executable code further includes, where the specification is too complex to generate executable code directly, means for refining a method by specifying a series of operations to be undertaken, to produce a refined method and for verifying that the refined method behaves in accordance with the abstract specification before generating executable code.

15. A system as claimed in claim 14, wherein the means for refining the method includes means for providing an algorithm of program statements including postcondition statements.

16. The system as claimed in claim 13, wherein the means for running and evaluating the executable code, further includes, where the code does not meet requirements, for identifying the defects and for correcting the abstract specification and then for repeating checking the abstract specification for errors and verifying that the class has the expected properties.

17. A system as claimed in claim 13, wherein the means for evaluating the speed of performance, further includes, where the speed of performance is inadequate, means for restructuring data maintained by the class, adding variable declarations for the restructured data, and refining the methods and constructors to take account of the restructured data and generating executable code.

18. A system as claimed in claim 13, wherein the means for evaluating the speed of performance, further includes, where the speed of performance is inadequate, means for refining the method to produce a refined method and verifying that the refined method meets the specification of the original method, and generating executable code.

19. A system as claimed in claim 13, wherein the abstract specification includes a name of the class, a list of other class or classes and/or interfaces that said class inherits from, an abstract model of data maintained by the class, abstract specification of the methods and constructors of the class, and theorems of expected behaviour of the class and the methods and constructors.

20. A system as claimed in claim 19, wherein the abstract model of data includes declarations of abstract variables and may optionally include class invariants which are conditions concerning values of the abstract variables that are expected always to be true and declarations of abstract methods private to the class that assist in defining the class invariants and what other methods achieve.

21. A system as claimed in claim 19, wherein the abstract specifications of the methods and constructors of the class include:

a method name;

a method parameter list; and

a definition of what the method achieves.

22. A system as claimed in claim 21, wherein the abstract specifications of the methods and constructors of the class further include one or more of a method result type, a precondition that is required to hold whenever the method is called;

and a post-assertion description of conditions expected to hold when the method returns.

23. A statement as claimed in claim 19, wherein a description of the class is divided into regions;

an abstract region containing the abstract data model and also private methods and constructors referred to elsewhere in specifications of the class;

an internal region containing re-implemented data and redundant data and also private methods and constructions referred to in re-implementations of other methods;

a confined region of methods and constructors that are used only within the class and within other classes that inherit from that class; and

an interface region of methods and constructors accessible to any program or components that uses instances of the class.

24. A system as claimed in claim 13, wherein the means for generating executable code includes means for:

xii) tokenizing the abstract specification to form a token stream and building a presentation of the abstract specification;

xiii) passing the token stream;

xiv) binding identifiers and operators to declarations;

xv) converting the specification and expressions contained therein to standard forms;

xvi) generating a new instance of each variable at every point which the variable is changed, effectively replacing each variable by a succession of constants;

xvii) generating proof obligations represent requirements for program correctness;

xviii) proving the obligations;

xix) using the abstract specification to generate a test harness or a set of test data for testing speed of performance;

xx) generating code statements to implement the specification where no code is provided;

xxi) translating the code statements to easily translatable form; and

xxii) translating easily translatable form to an output language.