[SystemSafety] Safety Culture redux

[Les Chambers]

David
A random thought. Are we heading in the general direction of using ontologies to describe the 
semantics of code. For example, given a contract of type X we need to see an aggregate of type 
a, b, c constructs in the code?
Les
> Steve,
> 
> Data abstraction and refinement has been well-covered in tutorials and
> texts on VDM and Z. For C and C++ I have only a few small examples that
> are public, such as the one in this conference paper:
> http://eschertech.com/papers/CanCPlusPlusBeMadeAsSafeAsSpark.pdf.
> 
> Regards
> 
> David Crocker, Escher Technologies Ltd.
> http://www.eschertech.com
> Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
> 
> On 26/02/2018 19:27, Steve Tockey wrote:
> > David,
> > Very interesting. One question. On your web site
> > (http://www.eschertech.com/products/verified_dbc.php), you say,
> >
> > “Contracts are most naturally and simply expressed in terms of a simple
> > abstract data model of a class”
> >
> > Where can I find more detail on that “simple abstract data model of a
> > class”? There could be some interesting synergy between that model and
> > something that I have been working on.
> >
> >
> > Thanks,
> >
> > — steve
> >
> >
> >
> > -----Original Message-----
> > From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
> > on behalf of David Crocker <dcrocker at eschertech.com>
> > Date: Monday, February 26, 2018 at 11:04 AM
> > To: "systemsafety at lists.techfak.uni-bielefeld.de"
> > <systemsafety at lists.techfak.uni-bielefeld.de>
> > Subject: Re: [SystemSafety] Safety Culture redux
> >
> > Steve, there are annotated static analysis techniques such as Escher
> > C/C++ Verifier (disclosure - a product from my company) and SPARK that
> > can do exactly that kind of semantic analysis, i.e. verify that each
> > function satisfies its contract - and that all callers to that function
> > satisfy their side of the contract too.
> >
> > David Crocker, Escher Technologies Ltd.
> > http://www.eschertech.com
> > Tel. +44 (0)20 8144 3265 or +44 (0)7977 211486
> >
> > On 26/02/2018 18:43, Steve Tockey wrote:
> >> Mario,
> >> You wrote:
> >>
> >> ³As far as I can see, the issue with static analysis is that
> >> there is a wide bandwidth of approaches available under this name. Some
> >> are good, some are outdated, some are inappropriate. The good ones that
> >> we desire to use, I believe, rarely come at low cost. On the contrary,
> >> these, even if sold as tools, require high skills and a lot of
> >> experience to be effective.²
> >>
> >> My concern is that these static analysis tools are only able to do
> >> structural (aka syntactic) analysis of the code. They are completely
> >> unable to do any significant semantic analysis of the code. As a simple
> >> example, the declared contract of a function might be that it requires X
> >> and guarantees Y but the analyzer is unable to tell me that the method
> >> code is consistent (or not) with that declared contract.
> >>
> >> Said a slightly different way, ³They call them bugs. We are trying to get
> >> everyone to call them defects (or, errors). But they really are just
> >> semantic inconsistencies². In order to be capable of finding the kinds of
> >> problems I care about, the tools need to be able to do semantic analysis
> >> of the code and that¹s orders of magnitude more difficult.
> >>
> >>
> >> Cheers,
> >>
> >> ‹ steve
> >>
> >>
> >>
> >> -----Original Message-----
> >> From: systemsafety <systemsafety-bounces at lists.techfak.uni-bielefeld.de>
> >> on behalf of Mario Gleirscher <mario.gleirscher at tum.de>
> >> Organization: Technical University of Munich
> >> Date: Saturday, February 24, 2018 at 6:39 AM
> >> To: "systemsafety at lists.techfak.uni-bielefeld.de"
> >> <systemsafety at lists.techfak.uni-bielefeld.de>
> >> Subject: Re: [SystemSafety] Safety Culture redux
> >>
> >> Dear Peter,
> >> dear all,
> >>
> >> Thanks for indirectly bringing up one of the many reasons why we started
> >> our survey on finding out the use of techniques known as formal methods
> >> (and, hence, many don't like them because of just the name which I think
> >> is sooooo sad) in various realms of software engineering practice. Last
> >> time I unintentionally triggered quite a discussion and would like to
> >> apologize for my insistence.
> >>
> >> Because Steve pointed at a classic (https://doi.org/10.1109/TDSC.2004.2)
> >> terminology issue "bug vs. error vs. defect", I'd like to remind those
> >> who haven't participated of our survey and kindly ask all of you to
> >> forward the link below to software practitioners who might be eligible
> >> to participate:
> >>
> >>
> >> https://docs.google.com/forms/d/e/1FAIpQLScMbKk3SDY62fzBujtJA-i8XKREZP40Mj
> >> X
> >> jIZvluZSVO9-QXA/viewform
> >>
> >> Accompanying a mindset change through good terminology, we also need
> >> empirical studies on finding out causes of the actual social phenomena
> >> we are discussing. We have gained almost 100 responses, however, this is
> >> by far not enough.
> >>
> >> Systems are eating the world and there is no time at all to stick around
> >> and rely on anecdotal evidence on "best practices."
> >>
> >> @Steve: As far as I can see, the issue with static analysis is that
> >> there is a wide bandwidth of approaches available under this name. Some
> >> are good, some are outdated, some are inappropriate. The good ones that
> >> we desire to use, I believe, rarely come at low cost. On the contrary,
> >> these, even if sold as tools, require high skills and a lot of
> >> experience to be effective.
> >>
> >> Thank you and have a nice weekend,
> >> Mario
> >>
> >> On 23.02.2018 12:00, Peter Bernard Ladkin wrote:
> >>> It is not just schools. I had a recent experience.
> >>>
> >>> Recent graduate in math with minor in informatics, now working at a
> >>> company in which programs and
> >>> sells WWW-based services. They are using Scala, which has some
> >>> functional programming facility. He
> >>> thinks of using type theory (that is, mathematical type theory, not data
> >>> typing) to improve the
> >>> "correctness" (his word) of the programs. Are we interested?
> >>>
> >>> Here is a simplified dialog:
> >>>
> >>> Me: "Is there a requirements specification of the program you are
> >>> interested in?"
> >>> Him: "What's that?"
> >>> Me: "It is a description of what you (or someone) wants the program to
> >>> do"
> >>> Him: "Oh, I don't think so"
> >>> Me: "You used the term <correctness>. If there is no description of what
> >>> you want the program to do,
> >>> what did you mean by <correctness>?"
> >>> Him: "It means the program is working the way we want it to work"
> >>> Me: "But didn't you just tell me there was no description of that?"
> >>> Him: "Huh?"
> >>>
> >>> And this from someone who is, as far as I know, quite smart and quite
> >>> capable. In any case, I did
> >>> have the impression he was less interested in this aspect of things than
> >>> in the prospect of playing
> >>> around a bit with type theory. That's fine. (But it's not what I do any
> >>> more.)
> >>>
> >>> I have had such experiences regularly over thirty years of teaching.
> >>>
> >>> PBL
> >>>
> >>> Prof. Peter Bernard Ladkin, Bielefeld, Germany
> >>> MoreInCommon
> >>> Je suis Charlie
> >>> Tel+msg +49 (0)521 880 7319  www.rvs-bi.de
> >>>
> >> _______________________________________________
> >> The System Safety Mailing List
> >> systemsafety at TechFak.Uni-Bielefeld.DE
> > _______________________________________________
> > The System Safety Mailing List
> > systemsafety at TechFak.Uni-Bielefeld.DE
> >
> 
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE



--
Les Chambers
les at chambers.com.au
+61 (0)412 648 992