Re: SPARK - Bubble Sort on Rosetta Code

[Phil Thornley <phil.jpthornley@gmail.com>]

On 27 Aug, 08:57, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 26 Aug, 23:32, Simon Wright <si...@pushface.org> wrote:> Phil Thornley <phil.jpthorn...@gmail.com> writes:
> >                                        ... I ask because of
>
> >       --# check A'Last <= A'First -> A'Last = A'First;
>
> That's an example of a 'tactical' check annotation that helps with
> proing some of the VCs. (It converts a potential path into an
> infeasible one, which makes it a lot easier to prove the post-
> condition.)

I thought about that a bit more and realised that it isn't necessary.
(Must have got left there from an earlier version of the code.)

So I've removed it from both of the versions it appeared in.

Cheers,

Phil