|
|
|
| Authored by: Anonymous on Monday, October 15 2012 @ 03:56 PM EDT |
I wasn't talking about "developing systems to analyze
software for correctness" ( That has many problems ). I was talking about
how you check the correctness of the program you are developing.
And that is possible to do. If it were not programming would be an exercise in
futility.
[ Reply to This | Parent | # ]
|
| |
| Authored by: cjk fossman on Monday, October 15 2012 @ 09:36 PM EDT |
Trying to resuscitate some very ancient learning here ...
It is possible to do a more strenuous code evaluation than
running test cases with "typical" values.
It consists of defining code preconditions and
postconditions, then walking through the code to verify the
code handles missing preconditions, that each precondition
is an actual requirement, and that the code yields the
defined postconditions.
Then walk through the code backwards to verify you get back
to the preconditions.
Obviously doing this for every line of code is an
intractable problem.
Back when I studied this stuff, flight software needed to be
verified to the branch level; that is, you had to be able to
prove that every branch in the code could be reached. This
is sufficient to prove, for example, that all your loops
will terminate and you have no divide by zero errors.[ Reply to This | Parent | # ]
|
|
|
|
|
