[SystemSafety] Modelling and coding guidelines: software components

[David MENTRE]

Hello,

Le 17/03/2016 10:22, GRAZEBROOK, Alvery N a écrit :
> On the principle of nudging folk in the right direction, it seems to me that the use of non-executable annotations (e.g. SPARK) is a valuable contribution for defining a library interface contract that would make software component re-use more checkable.
>
> Does anyone know of similar annotation schemes on language subsets of C, C++ or other more widely used languages?

B Method is not a widely used language but has a similar annotation 
scheme. It is used widely throughout the world by Siemens and Alstom for 
their CBTC (Communication Based Train Control) and (railway) 
Interlocking projects (see 
http://www.clearsy.com/wp-content/uploads/carte-monde-b-fr.jpg). It 
allows to re-use and adapt the software to a new context while knowing 
precisely what your are breaking.

Coming back to a previous point in a discussion, formal contracts (i.e. 
what your are calling non-executable annotations) is a way (the only 
way?) to precisely define what is the "environment" (i.e. the 
assumptions) of your program and know when you can re-use it or not.

The only issue with this approach is the cost and the technical 
complexity. A very few organisations are ready to pay that cost. I think 
some lest powerful approaches but less costly could be more widely used.

Best regards,
david