[SystemSafety] proofs

[Steve Tockey]

Paul,
Are you familiar with “Design by Contract”? Much of what you are talking about for abstract function-level behavior can be expressed in Design by Contract form. The missing piece would be artifacts of implementation choices (e.g., because an unsigned short was used inside the function, a maximum of 128 things can be supported).

It could be that a well-stated contract together with an explicit statement of technical limits could be sufficient.

The next question would be, “What about when the code is much bigger than a single function?”


Cheers,

— steve 


发自我的 iPad

> On Nov 23, 2018, at 3:42 AM, "paul_e.bennett at topmail.co.uk" <paul_e.bennett at topmail.co.uk> wrote:
> 
>> 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..
> ********************************************************************
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
> Manage your subscription: https://lists.techfak.uni-bielefeld.de/mailman/listinfo/systemsafety