[SystemSafety] Modelling and coding guidelines: software components

[José Faria]

Alvery,

>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,
http://frama-c.com/acsl.html

For C#, there's Spec#, from Microsft,
http://research.microsoft.com/en-us/projects/specsharp/

For Java, JML,
http://research.microsoft.com/en-us/um/people/leino/papers/jml-sttt.pdf

Best,
José



On Thu, Mar 17, 2016 at 9:22 AM, GRAZEBROOK, Alvery N <
alvery.grazebrook at airbus.com> wrote:

> 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 TechFak.Uni-Bielefeld.DE
>



-- 
--
*José Miguel Faria*
*Educed *- Engineering made better
t: +351 913000266
w: www.educed-emb.com
e: jmf at educed-emb.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20160317/33c7709f/attachment.html>