From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: 103376,55ae3803eb91d6ca X-Google-Attributes: gid103376,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news1.google.com!Xl.tags.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local01.nntp.dca.giganews.com!nntp.posted.plusnet!news.posted.plusnet.POSTED!not-for-mail NNTP-Posting-Date: Mon, 16 Mar 2009 05:29:30 -0500 Date: Mon, 16 Mar 2009 10:29:26 +0000 From: Tim Rowe User-Agent: Thunderbird 2.0.0.19 (Windows/20081209) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Ada UK conference: SPARK safety: is no delivery better than 1 defect? References: <355dc49a-3414-4883-a268-fa3bcc493e7b@o11g2000yql.googlegroups.com> <62pvl.120778$EO2.21395@newsfe04.iad> In-Reply-To: <62pvl.120778$EO2.21395@newsfe04.iad> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-yPqHI/tGD17THxAPn8Ufc/V23JicENbHC0oLU9pJpa2MNIDF7U6LKSnfmZ50zQu69kFW3HZmcjYkpvf!t0zjkTW08bxCmxrAIuekiNsVzl1EytUadwI5wB/4RaaDPmDyXi8s65xjvgMq6jjf1gIaqbTdCcPb!Ide7U6J20X2Y X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.39 Xref: g2news2.google.com comp.lang.ada:5112 Date: 2009-03-16T10:29:26+00:00 List-Id: Michael wrote: > "Ludovic Brenta" wrote in message > news:355dc49a-3414-4883-a268-fa3bcc493e7b@o11g2000yql.googlegroups.com... >> I read your post three times and I still can't figure out what your >> point is. >> >> You claim that "iFACTS has failed as an engineering results" > >> -- >> Ludovic Brenta. > > Hi Ludovic, > > Made it "CAATS" and you get what Nav Canada is reporting in its latest > Operation Strategic Plan. section - 08T.4, page 53. > http://www.navcanada.ca/ContentDefinitionFiles/Publications/CorpPublications/AdditionalPublications/Ops_Strategic_Plan_2008_2011_en.pdf [detail snipped] You are still not making clear what you think the cause of the delays in these projects is (well, you seem to be saying that it's Ada + formal methods, but not saying in what way they are the problem). I don't know what CAATS is, but I have some knowledge of iFacts, and one of the things I know is that it very difficult indeed to define how it should work. It's hard to specify, and it's hard to determine whether algorithms are adequate. Each of those (related) issues could lead to delays (or even failure) that have nothing to do with the language or the use of formal methods. Using Ada with formal methods you can have a great deal of confidence that an algorithm is correctly implemented, but if you don't have confidence that the algorithm correctly solves your problem then where's the value? This is certainly an issue for development of complex systems, but it's not an Ada or formal methods issue. I don't know whether this is the actual issue with iFacts, but it should be enough to show that "Ada + formal methods project has difficulties" doesn't necessarily mean that the difficulties are with Ada or formal methods. If you think Ada or formal methods is causing the difficulty, could you clarify why you think that, and explain what the specific issues are?