Re: SPARK : third example for Roesetta - reviewers welcome

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Le Sun, 15 Aug 2010 20:42:27 +0200, Phil Thornley  
<phil.jpthornley@gmail.com> a écrit:
> in http://www.sparksure.com/resources/Rosetta_Binary_Search.txt


> else
>    -- Switch to lower half subrange.
>    Upper := Position - 1;
>    Position := (Lower + Upper) / 2; -- <<<
> end if;
>-- [...]
>else
>    -- For "Middle <= Upper" in loop assertion.
>    -- Switch to upper half subrange.
>    Lower := Position + 1;
>    Position := (Lower + Upper) / 2; -- <<<
> end if;

Interesting to note: you moved “Position := (Lower + Upper) / 2;” inside  
logical branch, I suppose to ease prove, as the instruction is right in a  
context which makes its validity more obvious. This is indeed better than  
the idea of the factorization I used.

This topic makes me think about the latter about the Middle variable  
turned into a direct use of Position. May be I did "automatic useless  
optimization" here.

That is funny, because it happens I do the same (that is why I suppose I  
was not so good here due to a kind of "inappropriate automation").