Create error free database systems faster
A new and innovative axiomatic reasoning theory to create provable specifications.
Why is Specify4IT needed?
Create code without error
Creating “right first time” software for large modern programs is almost impossible, and users are continually frustrated by needing to install patches and updates. This is not an easy issue to solve as modern programs and programming languages are often too complex to be fully understood and checked by individual programmers. Often clients cannot specify their needs clearly, precisely, and unambiguously, making it difficult for the programmer to create code without errors.
Why are existing methods inadequate?
Testing the code
For database systems, existing methods rely on testing the final code to ensure that it complies with the specification. However, this can require hundreds of hours of coding to be completed before any error is found. Fixing the errors also requires significant time and cost. Even then clients may change their minds when they see the system working!
Testing is not proof of correctness
We should note Professor Dijkstra’s warning that: “Testing can show the presence of errors but never their absence”.
The fact is that programming is a complex, labour-intensive and error-prone process. If a specification cannot be proven to be correct, the resulting software cannot be proven to comply with the specification.
Formal methods
An alternative would be to use Formal Methods, such as Z or B languages. However, these are really only in the domain of highly qualified experts with formal maths and logic training.
A better way
What if there was a way that a software specification could be created that was proven to be correct, validated by the customer, and the system behaviour checked prior to any code being generated, and accessible to all programmers?
What does Specify4IT deliver?
Specify4IT creates error free database systems faster, mathematically provable, in exact accordance with the required specifications.
Mathematical proof of correctness
This is achieved by expressing the specification in a very structured manner; defining the system as a set of processes, interconnected by rules, and triggered by events. In this way, a specification is created that can be mathematically checked for consistency, and its behaviour can be assessed, and animated to ensure correctness, and compliance to the specification can be proven. All before any code is generated.
Specify4IT can then use this mathematically defined specification, which has been agreed by the client, and automatically generate error free code.
How does Specify4IT do this?
Highly innovative
The Specify4IT automated toolset uses a new and innovative axiomatic reasoning theory for provable software (named Predict) to enable this revolution in software creation.
Prior to any code generation, Specify4IT allows the user to:
Check
Check that all aspects of the specification are consistent and that there are no conflicts.
Animate
Animate the behaviour embodied in the user specification, so that a user can assess what happens in all situations.
Deduce
Deduce the application requirements, for comparison with the original instructions from the customer.
Prove
Prove the properties of the application.
Animation, deduction, and proof of the specification are automatically completed. The actual code for the specific application is generated automatically - in a matter of minutes.
Specify4IT ensures specifications are Complete, Consistent, Correct and Comprehensible and this has been independently verified with Imperial College London.
“Specify4IT is able to provide a higher degree of certainty that the software will behave correctly under all possible inputs and conditions.”
Testimonial by the independent examiner
"Specify4IT would be very beneficial in developing software for safety-critical and high assurance systems, particularly in industries where the reliability and security of software is paramount.”
Testimonial by the independent examiner
What are the benefits?
Time to deliver can be halved compared to conventional methods
In summary, Specify4IT enables:
1. Improved productivity
The creation of high-quality database software more quickly and with significantly reduced costs, resulting in improved productivity and profitability.
2. Error free software
The use of this new and innovative axiomatic reasoning system enables every user to create accurate specifications that result in error free software. Once specified an application can be delivered within hours of its specification being complete.
3. Halving the time
We estimate that database projects created using Specify4IT will only require half the staff for half the time to achieve successful delivery, compared to a conventional approach.