Re: {Pre,Post}conditions and side effects

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 22.12.14 20:38, sbelmont700@gmail.com wrote:
> Now you've got a function that doesn't access any global variables, but not only randomly exhaust the heap, but also permanently blocks the thread, so you are right back where you started.

A function call can "cause" even more, pure or not. Any Ada
check can have effects.

Add to Randy Brukardt's response that everything manipulates
"the program"'s state. Invoking any function can also exhaust
resources, e.g. hit the stack limit. But that's then the catch
all Standard.$Runtime$_Error.

However, there are two notions to keep in mind, I think:

1. Contract based design, or at least Design by Contract™, entails
a proof obligation(*).  Without it, the former is sill a very useful
debugging tool, or testing tool.

2. The model of contract based design should not be confused with
its implementation, I think: For example, the checks may be performed
on a multiprocessor computer in such a way that one of the processors
checks a copy of a sequential program, while the other does not check.

There might be theoretical corner cases where duplication is not
possible. It might be impractical to detect important differences
in the copies' states, but you get the idea, in particular with (1)
in mind: proof obligations.

In fact, a duplicated setup does not seem to be entirely dissimilar
from redundant installations already in use?

__
(*) At Ada Europe 2012, Betrand Mayer explains that Eiffel programs
in production are supposed to run with checks disabled.