At 07:31 03/05/2013, you wrote:
Problem is, how do I prove to the customer/user that it is working as
expected no matter what?
There are two important points in your question.
The second (!) is "prove".
The first is "as expected".
Let me expand on why. For a system (irrespective of its nature or
implementation technology) to be "working as expected", you first have
to define exactly how it is expected to behave in every situation it
may encounter. That's called functional specifications. Specs need to
be complete and deterministic down to the lowest levels (of spec, not
implementation!) to be useful later. If you want to "prove" something
based on these specifications, you need to express them as a formal
model by using one of the formal methods available. This model needs to
be proven complete (no unspecified state) and non-contradictory under
the formal methodology used.
Once you have formal specifications defined as a formal model (we call
this a "machine" in B) you can enter the process of refinement. To
refine a formal model is to gradually introduce every aspect of
implementation while using adequate proofing tools to demonstrate (and
here I mean "mathematically") at every step that the refined specs are
mathematically consistent with the initial formal specs. Actual large
systems require many refinement steps to achieve a final implementable
model (B0 in the B method).
Once here and if the method chosen has the capability, you can actually
produce executable code (typically secure ADA or C) for a given
hardware target, along with a formal proof that the executable will
behave "as expected" in all aspects. B is such a method.
The excellent news is that you don't need ANY test step: just deliver
the production to the client, re-play the proof before him, get payed
and fly to some sunny place with white sand beaches and no phone or
Internet for a well deserved rest. There exists a valid mathematical
proof that the production will always work "correctly", that is
conforms to the initial formal model, in every aspect.
The less pleasant point is that a complete coverage by a top-notch
formal method is really hard: you need experts in this method and ample
time. The "simple" initial formal model is the first hard work because
the human language --even used for specifications-- is incredibly
ambiguous in practice and more than often uses implicit references to
untold implementation details left vague (e.g. implicit "knowledge"
about the behavior of the underlying OS for a software product).
What you do when you use a formal method is that you merge the two
branches of the V development process. In fact, you intermix tests (the
right branch of the V) which translate into proof of correctness, with
the classical development right branch.
Many real-world systems requiring high dependability for
mission-critical applications have shown that the time invested in
refinements (where most of the time and efforts are used) grossly
balance the time and efforts normally spent on incomplete or
unconclusive tests and, after release, in fixing issues left over and
discovered in the wild. Of course with a formal development you benefit
of a program proven correct by construction.
SQLite would be a very good candidate for a formal development if its
design was not somehow a moving target. I'm not saying DRH and his team
are amateur developpers, all I mean is that when significant new
features are introduced in the user specifications, the whole formal
process has to be restarted. Many of the changes introduced in SQLite
over the last few years have deep implications on its behavior.
Depending on how the changes introduced fit the formal model or can't
cope with its structure, a new version may require much work, up to
complete rework. Formal methods are best suited for fixed
specifications applications.
In short, "yes you can" reach part of your goal, but if you take your
own words "prove" and "working as expected no matter what" at face
value, then you definitely heavyweighted formal methods to prove your
application, the OS and the hardware all this runs on, possibly using
redundant (majority) architecture or a secure coded processor. Needless
to say, this is overly expensive for most applications.
JcD
_______________________________________________
sqlite-users mailing list
sqlite-users@sqlite.org
http://sqlite.org:8080/cgi-bin/mailman/listinfo/sqlite-users
