Seeking Input for Software Verification Policies?

e8johan asks: "I currently work at a company in the automotive industry. It is importat to ensure quality and for our products we use extensive testing before, during and after the assembly. Now I have been asked to help in the creation of a company instuction for ensuring that all 'in-house' developed software works properly. I have written a short summary describing the essentials such as: "do not ignore compiler warnings", "always describe what the code is intended to do in your comments", "do not assume that all users run in the same environment", etc. I now feel that I need more input, has anyone done anything like this before? How do you test your software?"

Comments

Testing or proving?

[heliocentric]

There is a system where if you set your pre and post conditions well you can mathematically prove your code performs what is asked. You "simply" drag your post conditions up your code and if you arrive at a set where the pre conditions are at least a sub set, then you know if the input matches the post conditions will also be satisfied.

You need good things like loop invariants, and deep thought about what you wish to limit yourself to. But, if you start at the base procedures and work to building up to the ones that call these then you can work your way up to "if the input from user matches..." and then put in tons of good input checking and you're solid.

Now, this takes lots and lots of time, but maybe this is the sort of things you're looking to do. I used this method in designing an e-voting system to prove that things were encrypted properly and that the system would be stable.

Fun stuff.