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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!Xl.tags.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail NNTP-Posting-Date: Mon, 27 Jul 2015 21:41:18 -0500 Subject: Re: Handling transactions? Newsgroups: comp.lang.ada References: <6b5c318e-430d-4950-9762-e0ecdaa0ac9a@googlegroups.com> <9976ca19-a558-4f4e-80d3-a9b37ee07326@googlegroups.com> From: Norman Worth Date: Mon, 27 Jul 2015 20:41:19 -0600 User-Agent: Mozilla/5.0 (Windows NT 6.3; WOW64; rv:38.0) Gecko/20100101 Thunderbird/38.1.0 MIME-Version: 1.0 In-Reply-To: <9976ca19-a558-4f4e-80d3-a9b37ee07326@googlegroups.com> Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Message-ID: X-Usenet-Provider: http://www.giganews.com X-Trace: sv3-0q2zXCfi1GowRYKeQG+zu8e1CeaZndMbOKNOZuXYyr38WnDVDKugZd4R2lnsh5MOoJsGafSnQu1WSJ/!9euZHvHXvBiLgP5cagh7Gs+wvd0vpXhRF/u2qMchQIGVamnd3A4CICGi67KT83iONnDUokmsH78= X-Complaints-To: abuse@giganews.com X-DMCA-Notifications: http://www.giganews.com/info/dmca.html 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.40 X-Original-Bytes: 2634 Xref: news.eternal-september.org comp.lang.ada:27063 Date: 2015-07-27T20:41:19-06:00 List-Id: On 7/27/2015 10:38 AM, David Botton wrote: >> One approach to high-integrity systems requires you to prove, using for >> example SPARK, that there can be no exceptions; then the problem doesn't >> arise. > > SPARK isn't Ada nor is it an approach the makes sense for most programming tasks. He could also just write those sections in other proof base languages. I wonder if SPARK is even the best choice today for that purpose. > > EGarrulo, your question is not a language question but a design question. What you want can be done in any language and depending on what you are trying to "roll back" I can think of many many ways to do it. Be specific and I'm sure some of us can offer advice for your project. > > David Botton > Proving that an exception is impossible is nice when you can do it. (And you can do it outside of SPARK.) Unfortunately, that is not always the situation. Problems caused by data coming from an I/O stream are common examples of why transactions fail. Using preconditions to check the data used to call a transaction procedure can simplify matters, but rolling back just what needs to be rolled back can still be messy. However, the general method shown for databases should work for just about everything.