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:
> I decided that it would more interesting to strengthen the post-
> condition to say that 'not Success' means that no element in Source is
> equal to Item.

After I have read this, it is more clear :


>    --# post (Found -> (Source (Position) = Item)) and
>    --#      (not Found ->
>    --#         (for all I in Index_Type range Source'First .. Source'Last
>    --#                                  => (Source(I) /= Item)));

This is indeed a more strong/strengthened postcondition than mine. To talk  
with a word I like : this is more expressive.


>    --# assert not Terminated and
>    --#        Lower >= Source'First and
>    --#        Upper <= Source'Last and
>    --#        Position >= Lower and
>    --#        Position <= Upper and
>    --#        not Found and
>    --#        (Lower > Source'First -> Source(Lower - 1) < Item) and
>    --#        (Upper < Source'Last -> Source(Upper + 1) > Item);

Interesting to study: you could move all in the loop assertion.


(I am still going on with reading)