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=0.2 required=5.0 tests=BAYES_00,INVALID_MSGID,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: fac41,f66d11aeda114c52
X-Google-Attributes: gidfac41,public
X-Google-Thread: 103376,f66d11aeda114c52
X-Google-Attributes: gid103376,public
From: Joachim Durchholz <joachim.durchholz@munich.netsurf.de>
Subject: Re: Building blocks (Was: Design By Contract)
Date: 1997/10/01
Message-ID: <34329773.B05F348B@munich.netsurf.de>#1/1
X-Deja-AN: 277660720
References: <34316EC3.5B62@dynamite.com.au>
 <199710011402.QAA02444@basement.replay.com>
Reply-To: "joachim.durchholz@"@munich.netsurf.de
Newsgroups: comp.lang.ada,comp.lang.eiffel
Date: 1997-10-01T00:00:00+00:00
List-Id: <comp.lang.ada>


Anonymous wrote:
> 
> Certainly "while" is preferred by those doing program correctness
> proofs; all the techniques for this that I have seen have been for
> "while" loops. Avoiding "while" does usually make for more readable
> code. In this specific example, "while" requires a flag variable,
> which is less readable than using "exit".

Actually positive/negative logic has nothing to do with why the
correctness guys prefer "while". What they want is that the termination
condition is at the start of the loop.
Actually Eiffel doesn't use "while", it uses "until". The correct syntax
is:

from
  -- loop initialization - arbitrary code
invariant
  -- here goes the loop invariant, a boolean expression that's
  -- true whenever execution reaches the top of the loop.
  -- loop invariants are useful to prove the correctness.
variant
  -- here the loop variant - an expression that will decrease
  -- with every iteration.
  -- loop variants are useful to prove that the loop will terminate.
until
  -- put your termination condition here
loop
  -- statements to be repeated
end

The "from" part is just syntactic sugar - leaving away the "from"
keyword won't change the semantics. Still it's useful to indicate the
beginning of the loop set-up code - it's often rather contrived to force
the loop invariant on the first go through the loop.

"invariant" and "variant" are the algorithm prover's tools. However,
proving and convincing somebody that it actually works is much the same,
i.e. these constructs are even useful when hacking. In particular if
you're in doubt wether your loop does exactly what it should, and wether
it terminates at all! Remember your first attempts at binary search in
an array?

The above construct has interesting properties (which will be well-known
to algorithm provers):
1. If a variant is present the code is guaranteed to terminate. Quite
useful for loops.
2. The loop invariant will be true at the start and at the end of the
code of the loop body.
3. When the loop terminates, both the invariant and the termination
condition will hold. Usually you don't have to look at the loop body to
understand what the loop is doing.
4. When reading a loop without the invariant stated, the worst problem
for understanding the code is this: We know numerous conditions that are
true when execution reaches the top of the loop, but we don't know which
of these conditions will be destroyed by the loop body. So we don't
understand which conditions will still hold for the second iteration,
i.e. we don't know what conditions the code of the loop body assumes.
This makes understanding the code extremely difficult - this is much
like reading the body of a routine without being allowed to look at the
parameter and local variable declarations (actually I think it's worse).

Regards,
Joachim
-- 
Please don't send unsolicited ads. (The @@ is for confusing spambots.)