Awesome

gistfile1.txt

          -=-=-=-  Andrew and Skye's Awesome Adventures: -=-=-=-
         -=-=-=- Question 2: Counterfeit Coin Correctness -=-=-=-

Loop invariant:

    At the beginning of each recursion, the real doubloon is either in pile
    A, B, or C.

Initialization:

    Since piles A, B, and C are collectively exhaustive and mutually
    exclusive, it is trivial to see that the gold doubloon is amongst them.

Maintenance:

    We will weigh piles A and B and return the heavier of them, unless they
    are the same weight, in which case we will return pile C.

Termination:

    The recursion ends when a pile of size 1 is returned, which must be the
    real coin.