I tend to agree that having the extra classes is clearer than not having
them. This clarity, however, does have its price (the extra classes
themselves) so I suppose it depends on the problem being solved (what
doesn't?).

And as a slight aside, OO for me is more about encapsulating variation (be
that behavioural or data) than pure data encapsulation. Of course, to each
his own.

snip

Well, as you ask, I've been trying to think of encounters I've had that are
relevant to your question, and I think I've spotted one - but in this case,
the classes are very simple, perhaps so much so that they bare no true
relation to your own classes: you must be the judge. Again, I find myself
thinking that the nature of the problem itself decides.

Anyway, I've a little poker game that offers three different levels of
computer opponent, called a Type 1 AI, a Type 2 AI and a Type 5 AI. The
game's configurable via a BinaryOption class, and I've three subclasses
called Type1AIOption, Type2AIOption and Type5AIOption that say whether a
particular AI is allowed to play in a particular game:

http://www.edmundkirwan.com/servlet/fractal/cs1/code/package123.html

http://www.edmundkirwan.com/servlet/fractal/cs1/code/package124.html

http://www.edmundkirwan.com/servlet/fractal/cs1/code/package125.html

All these subclasses just assign variables in the base BinaryOption class
and contain no behaviour of their own.

I think, however, that Mister Lahman's advice has rubbed off onto me,
because in my current project I also use BinaryOption, and I presently have
six binary options, but I don't create six subclasses; instead, I pass the
parameters into the constructor of a, "Raw," BinaryOption:

   /**
    * Create the system options.
    */
   private void addAllOptions() {
       options.add(new AlgorithmOption());
       createBinaryOption(Configuration.DELETE_ORIGINAL_OPTION_NAME,
                          false, Configuration.MISCELLANEOUS_GROUP);
       createBinaryOption(Configuration.AUTO_CLOSE_PROGRESS_OPTION_NAME,
                          false, Configuration.MISCELLANEOUS_GROUP);
       createBinaryOption(Configuration.ALLOW_REENCRYPTION_OPTION_NAME,
                          false, Configuration.MISCELLANEOUS_GROUP);
       createBinaryOption(Configuration.WATERMARK_OPTION_NAME,
                          true, Configuration.MISCELLANEOUS_GROUP);
       createBinaryOption(Configuration.CHECKSUM_OPTION_NAME,
                          true, Configuration.MISCELLANEOUS_GROUP);
       createBinaryOption(Configuration.CBC_OPTION_NAME,
                          true, Configuration.MISCELLANEOUS_GROUP);
       Option viewOption = new ViewOption();
       options.add(viewOption);
   }

   /**
    * Creates a binary option with the given name, default value, and group
    * header identity.
    *
    * @param name binary option name
    * @param value default value
    * @param groupHeaderIdentity group header identity
    */
   public void createBinaryOption(String name, boolean value,
                                  String groupHeaderIdentity) {
       options.add(new BinaryOption(name, value, groupHeaderIdentity));
   }

So I'd have to say, on the whole, that I tend not to have subclasses which
differ from base classes only by data.

I wouldn't dream of contradicting a master such as Dijkstra, but I always
phased-out when it came to, "Predicate transformers." Some day I must look
into modal and predicate calculus to see what on earth it's all about.

I have often wondered, however, about the practicalities of program proofs.
Surely there's a circular argument in there somewhere, for how to we show
that the proof is correct?

If a proof is a page long, then I'd be happy to have an expert tell me it's
correct.

If it's fifty pages long, then I'd rather have a few experts confirm it.

If my program is one million lines long, however, how long will the proof
be? Ten thousand lines? How many experts are needed to guarantee that this
proof contains no errors?

Also, looking at a Dijkstran proof, I always find it looks like a program
itself, somehow condensed from the original. Could that proof itself be fed
into a computer and executed? If so, has the proof just, "Compressed," the
original program by some impressive factor (say 10, as above)? Can we ditch
the original and just use the executable proof?

And if we can do this, then how do we prove that the executable proof is
proven?

And can we make an executable proof of the executable proof that's an
impressively compressed factor of the (first) executable proof?