Re: [SystemSafety] Modelling and coding guidelines: software components

From: José Faria < >
Date: Thu, 17 Mar 2016 09:47:30 +0000


>Does anyone know of similar annotation schemes on language subsets of C,
C++ or other more widely used languages?

For C, I'd highlight ACSL, which is supported in the Frama-C platform,

For C#, there's Spec#, from Microsft,

For Java, JML,


On Thu, Mar 17, 2016 at 9:22 AM, GRAZEBROOK, Alvery N < alvery.grazebrook_at_xxxxxx

> 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? If this concept were to become
> more widely available, it could have a big impact on the expectations for
> "good quality" software components and be used in areas where regulations
> don't reach.
> Cheers,
> Alvery
> [snip]
> > Whether we like it or not we are all
> >involved in component based design. My experience with software
> >libraries is that there are some good ones out there that are quite
> >stable. On the negative side I have two problems with them:
> >1. They are almost universally very poorly documented so you can waste
> >a day trying to achieve a trivial outcome.
> I agree that many examples of software components I have seen have lacked
> sufficient documentation to be able to make sensible decisions about
> suitability. I find that if you can chuck it back via the author to get
> that improved, the documentation improvement is sometimes worthwhile.
> Otherwise you end up writing it yourself.
> >2. The authors seem to have no concept of backward compatibility.
> >If you make the mistake of upgrading to the latest version you can
> >trash your complete application: data structure changes, even method
> >name changes. Amazing!#
> Regression testing is part of the regimen and any new version has to pass
> all the old tests as well as any new ones. There is a strict notion of how
> much impact changes at lower levels will have on the upper layers of the
> application. I'll happily explain about surfaces to you at some stage.
> [snip]
> This email and its attachments may contain confidential and/or privileged
> information. If you have received them in error you must not use, copy or
> disclose their content to any person. Please notify the sender immediately
> and then delete this email from your system. This e-mail has been scanned
> for viruses, but it is the responsibility of the recipient to conduct their
> own security measures. Airbus Operations Limited is not liable for any loss
> or damage arising from the receipt or use of this e-mail.
> Airbus Operations Limited, a company registered in England and Wales,
> registration number, 3468788. Registered office: Pegasus House, Aerospace
> Avenue, Filton, Bristol, BS34 7PA, UK.
> _______________________________________________
> The System Safety Mailing List
> systemsafety_at_xxxxxx >

*José Miguel Faria*
*Educed *- Engineering made better
t: +351 913000266
e: jmf_at_xxxxxx

_______________________________________________ The System Safety Mailing List systemsafety_at_xxxxxx
Received on Thu Mar 17 2016 - 10:48:10 CET

This archive was generated by hypermail 2.3.0 : Tue Jun 04 2019 - 21:17:08 CEST