Problem: To Catch a Lion in the Sahara Desert.
1 [ f(z) ------- | --------- dz 2 \pi i ] z - \zeta Cwhere C represents the boundary of the desert. Its value is f(zeta), i.e. there is a lion in the cage [3].
As a variant let us assume that we would like to catch (for argument's sake) a male lion. We insert a tame female lion into the cage and apply the Heisenberg exchange operator [7], exchanging spins.
Axiom 1: Sahara elem deserts
Axiom 2: Lion elem Sahara
Axiom 3: NOT(Lion elem cage)
We observe the following invariant:
P1: C(L) v not(C(L))where C(L) means: the value of "L" is in the cage.
Establishing C initially is trivially accomplished with the statement
;cage := {}
Note 0:
This is easily implemented by opening the door to the cage
and shaking out any lions that happen to be there initially.
(End of
note 0.)
The obvious program structure is then:
;cage := {} ;do NOT (C(L)) -> ;"approach lion under invariance of P1" ;if P(L) -> ;"insert lion in cage" [] not P(L) -> ;skip ;fi ;odwhere P(L) means: the value of L is within arm's reach.
Note 1:
Axiom 2 ensures that the loop terminates.
(End of note 1.)
Exercise 0:
Refine the step "Approach lion under invariance of P1".
(End of exercise 0.)
Note 2:
The program is robust in the sense that it will lead to
abortion if the value of L is "lioness".
(End of note 2.)
Remark 0:
This may be a new sense of the word "robust" for you.
(End of remark 0.)
Note 3:
From observation we can see that the above program leads to
the desired goal. It goes without saying that we therefore do not have to
run it.
(End of note 3.)
(End of approach.)