Process and system for developing mathematically validated object-oriented software
AssigneeEscher Technologies Ltd
InventorDavid Crocker
Life of this patent
Estimating the term…
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.
Claims24
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.
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.
Dependencies are inferred from the claim text.