Re: Handling transactions?

[Norman Worth <nworth@comcastNOSPAM.net>]

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.