Given an array `A`.(0 ≤ `i` < `N`) of nonnegative integers, that is:

(0) ⟨∀i: 0 ≤i<N:A.i≥ 0⟩

and a positive integer `s` > 0, we want to find a segment of `A` that sums to `s`, if it exists. Define:

S.i.j= ⟨∑k: 0 ≤i≤k<j≤N:A.k⟩

The gematric search for `s` in `A` is to find, if possible, a pair (`p`, `q`) such that S.`p`.`q` = `s` (it is hoped that conoisseurs would readily make the connection). Note a number of things:

- S.
`i`.`j`is a total function on`i`,`j` - By definition, the sum on an empty range is zero:
(1) S.

`i`.`i`= 0for

*all*integer`i`. - For arguments in range of
`A`, S.`i`.`j`is monotone on its second argument and antitone on its first. That is, given 0 ≤`i′`≤`i`<`j`≤`j′`≤`N`:(2) S.

`i`.`j`≤ S.`i`.`j′`(3) S.`i`.`j`≤ S.`i′`.`j`

What should the result be if no such segment is present in `A`? One possibility would be setting a flag `found`, such that the program ensures:

¬found∨ S.p.q=s

An alternative would be to guarantee some condition on (`p`, `q`) equivalent by design to `found`. Given that `s` ≠ 0, one such condition would be satisfied by S.`p`.`q` = 0 as a suitable sentinel. By (1), this is implied by `p` = `q`, and we choose the weaker postcondition:

(4)p=q∨ S.p.q=s

Now (4) is trivially satisfied by:

{A.(0 ≤i<N) ∧s> 0 } gemsearch ≡p:= 0;q:= 0;sum:= 0; { reduce |sum - s| under invariance of (4) } {p=q∨ S.p.q=s}

where `sum` = S.`p`.`q` at each step. How should we meet the refinement obligation in the program? We clearly have three cases:

`sum`=`s`We have found our segment, and we can stop looking.

`sum`<`s`By (2) we can extend the segment on the right, provided we can, that is, if

`q`≠`N`.`sum`>`s`By (3) we can shrink the segment on the left, provided we can, that is, if

`p`≠`q`. But since`s`> 0, this is implied by`p`≠`N`, a weaker condition symmetric to the previous one and thus preferable. It is also suitable for the repetition guard, since its negation implies the postcondition.

We have:

{A.(0 ≤i<N) ∧s> 0 } gemsearch ≡p:= 0;q:= 0;sum:= 0;dop≠N∧sum≠s→ifsum<s∧q≠N→sum:=sum+A.q;q:=q+ 1 []sum>s→sum:=sum-A.p;p:=p+ 1 [] … → ?fiod{p=q∨ S.p.q=s}

The conditional is not exhaustive. Let's calculate what the obligations are for third case:

¬((sum<s∧q≠N) ∨sum>s) ≡ { DeMorgan, twice } (sum≥s∨q=N) ∧sum≤s≡ { Distribute } (sum≥s∧sum≤s) ∨ (q=N∧sum≤s) ≡ { Tertium non datur }sum=s∨ (q=N∧sum≤s) ⇐ { Loop condition }q=N∧sum<s

This condition expresses a deficient suffix of `A` which is, by (3), as large as it can be, hence we can quit the search. Left-factoring the common condition on `s`, we arrive at our final program:

{A.(0 ≤i<N) ∧s> 0 } gemsearch ≡p:= 0;q:= 0;sum:= 0;dop≠N∧sum≠s→ifsum<s→ifq≠N→sum:=sum+A.q;q:=q+ 1 []q=N→p:=Nfi[]sum>s→sum:=sum-A.p;p:=p+ 1fiod{p=q∨ S.p.q=s}

The algorithm is of complexity obviously linear on `N`, since no element of `A` is accessed more than twice.