How SPECIFY4IT Works
The SPECIFY4IT™ approach to specification demands more detail from the analyst than is usual and the checking the toolset undertakes is meticulous. PDT believes the extra effort to obtain correct, consistent and easily understood specifications leads directly to systems that:
- behave exactly according to their specification
- are reliable, of high-quality, and free from error
- are guaranteed to possess critical properties
- are deliverable within hours of the specification being complete
This reduces rework to correct errors and misunderstandings, speeds delivery to customers, and produces error-free systems that are reliable and ensure customer satisfaction.
The purpose of a software specification is to define an information system. It outlines the purpose and objectives of the system, and defines the way in which these will be satisfied.
The SPECIFY4IT™ approach to specification has four stages:
- prepare a high-level model of the system
- add detail
- the SPECIFY4IT™ toolset checks for consistency and correctness
- system construction and generation of running code converts information directly to a running system.
In the first stage PDT summarises your specification in a business model.
This model:
- Defines your required information system
- Shows certain inputs, performs some processing, and produces certain outputs (its behaviour must conform to the business rules of your organisation)
- Responds to events in the real world - it shows each business process (or process group) and the way information moves from one process to another
- Offers the immediate benefit of user understanding. Teams can recognise their own area of the business, know what they do, here their data comes from, and where it goes. This allows users to quickly identify and correct any business analysis errors.
Below is an example of a partial diagram during its preparation:
The softbox icons show individual processes (or process groups)
The arrows show the nature of the information flow (whether information either flows directly or is used only for validation).
The model can be manipulated by inserting or deleting either rows or columns; blocks can also be moved or copied from one part of the diagram to another.
The model can be copied, refreshed, or printed and the magnification changed so more or less of the model is visible at any one time.
On printout, the printout size can be adjusted to fit a single sheet or printed on a number of tiles that can be joined.
It is helpful to both analyst and users to prepare this model at an early stage. The diagram is generated by the tool to ensure that it remains a correct and accurate model of the business throughout the analysis process. The benefit is early identification and correction of any errors; this reduces re-work, and avoids work based on a faulty foundation.
Detail is added by completing standard forms. There are a number of different forms so the information provided whenever you complete a new form or amend a current form is stored (in mathematical form) in the specification repository (or knowledge base).
The form opposite allows you to define data associated with a particular process. Where possible, PDT provides pull-down lists from which users can make selections into the relevant windows. This saves repetitive data entry and precludes possible errors.
There are forms to allow users to represent data and objects, identify functional processing, and define business rules and events. All forms work in the same way: with pull-down lists to minimise typing, relevant buttons to allow selection and other operations as appropriate, and step-forward and step-back functionality to next and previous records.
The data entry part of the workbench does not constrain analysts either in what they enter or in how they choose to organise the entry process. Entry in logical order is not a requirement.
Specification Correctness Checking
- The specification can be checked for consistency at any point
- Inconsistencies must be corrected before undertaking any further checks
- The toolset produces a listing describing any errors
- The consistent specification can then be tested for correctness by animating it with example data. The toolset will show the behaviour of the system for any sequence of input events.
The result of testing a small portion of an (incomplete) model is shown below:
The text windows show various aspects of the reasoning process following the entry of each event during the test. It also shows the predicted content of each part of the system database at that point in the test.
The graphics windows show an overview of the whole system, with the locally active area highlighted and a more detailed view of the active area so that you can trace the reasoning process if required.
PDT has collaborated with Escher Technologies Ltd (ET) to provide provably correct code generation facilities. We translate a correct specification into the Perfect language and then use their proven code generator within the Perfect Developer toolset to generate code according to a set of rules.
The user benefit is high reliability and error-free code produced quickly, that matches the specification absolutely.
Other features of SPECIFY4IT™ code generation:
- Perfect Developer toolset will currently generate C#, C++ or Java code
- current format for code delivery is as a web browser-based client-server system using Java (other delivery formats can be considered)
- the Perfect Developer toolset contains a powerful automated theorem-prover. Part of our translation process includes deducing properties the system should possess, coupled with the automatic generation of corresponding proof obligations - users can provide additional obligations
- PDT guarantees that any generated system will support every proven property. PDT will correct any system that demonstrably breaches this guarantee.
Two screens from a warehousing example, show a user making an order entry. The system is about to adjust the relevant stock records as a consequence.
