[SystemSafety] proofs

[paul_e.bennett at topmail.co.uk]

On 23/11/2018 at 5:10 AM, "Steve Tockey" <Steve.Tockey at construx.com> wrote:
>
>Paul E. Bennett wrote:
>
>³As I know I have stated many times before, like hardware 
>components,
>software components need to be supplied with a descriptive data-
>sheet that
>explicitly states what the functionality of the component is²
>
>Do you have any thoughts on what the data-sheet like description 
>of the
>functionality of a software component should look like?
>
>
>Cheers,
>
>‹ steve

Considering that I may deal with software components on a much finer
granularity than many on this list (down to individual functions) I would
say that a comment block within the source for teh function should be
the least I would expect. Written in quite an imperative style of course.

At the very minimum it would declare the expected inputs and expected
output data items (along with what they represent), a note of the type of
transformation performed on the data items, the cell-width and style of
machine resource required. Then the limitations beyond which the
correct functionality is not guaranteed.

For an example, declaring that the function only operates for positive
integers and there is no guarantee of sensible result of the input data
becomes negative.

This way, you have something against which the selection of components
from a pre-written stock can be quickly evaluated for possible inclusion
and the data forms the basis for properly evaluating fitness for purpose.

Of course, you will still have the worry of what the compiler might do to
mash things up completely. In my case, The compilers I use are actually
part and parcel of the basis for my bare-metal up implementations and
I have a great deal of certainty of how they interact with the hardware.

Considering that, when you document at this level, even the good old
fashioned MK1 eyeball can often pick up problems during a review.

Regards

Paul E. Bennett IEng MIET
Systems Engineer
Lunar Mission One Ambassador
-- 
********************************************************************
Paul E. Bennett IEng MIET.....
Forth based HIDECS Consultancy.............
Mob: +44 (0)7811-639972
Tel: Due to relocation - new number TBA. Please use Mobile.
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************