[SystemSafety] Safety Culture redux

[David Crocker]

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
>