Re: {Pre,Post}conditions and side effects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Fri, 8 May 2015 18:31:02 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:8u3gz9fsuax7$.se3784kmjgvm$.dlg@40tude.net...
>> On Thu, 7 May 2015 13:32:28 -0500, Randy Brukardt wrote:
> ...
>>> You end up writing the program twice in two different languages.
>>
>> That is the idea. But it is not *the* program. The program is written only
>> once in Ada. The proofs are written *for* this program, they do not change
>> the program itself. Though proofs may hint the programmer to redesign
>> certain parts of the program.
> 
> That's madness. If the description is sufficiently complete to describe the 
> program (and it has to be for the proofs to mean much), then one could have 
> generated the program from that description and forget the Ada altogether 
> (and most people would do exactly that).

Except that no description ever complete. A more important thing is that
you could not convert such descriptions into code.

As an example consider a definition of sine from a text book. It
sufficiently completely defines sine, but gives you no idea what sin(0.76)
is.

The difference is in the computational framework. The behavior descriptions
are intended for the correctness prover. They program the prover, nothing
else. The behavior definitions (the program proper) are intended for the
machine. They program the machine. (The definitions from the text book are
for the framework which is not even computable)

> And there are few applications 
> where there is any value to writing the program twice; for most, it is just 
> wasted time.

Nothing is written twice. Proof specifications are as much program as test
code is. Don't you write tests?

> *Especially* if you're adding them after the fact -- what would 
> the point be? The program is already debugged and fielded.

Most interesting programs cannot be debugged. It is quite strange, you
don't believe correct program exist, but trust "debugged" programs do!
(:-))

> The only benefit 
> to any of these things is in shortening the debugging time, but once that's 
> already done, further work is pointless. (We had a rule at RRS about not 
> futzing with working code, because we'd been burned by that many times. It 
> was necessary to prevent people like me wasting lots of time on "cleanups" 
> that ultimately didn't clean up anything. As Tucker likes to say, you can 
> move the bump under the rug, but its rare that you can get rid of it.)

Adding proofs meant to happen much earlier than that. But, surely, I would
gladly add proofs to already deployed code. It is always worth to look
after potential problems.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de