WyIL: Significant Refactoring of VcGenerator.

The Verification Condition Generator (VcGenerator) is a significant part
of the verification process within the Whiley compiler.  As part of the
move to supporting compound bytecodes (e.g. for loops, etc) the
VcGenerator needed to be updated.  As part of that, I have gone further
and significantly redesigned and improved the algorithm.  This includes:

1) Better coherency between VcGenerator and VcBranch.  In particular,
all control logic is now moved within the VcGenerator, rather than being
spread over both classes.

2) Better support for generating verification conditions.  The
VcGenerator now constructs a "branch graph" from which verification
conditions are generated.  This allows for better reuse between
verification conditions themselves which will hopefully improve
efficiency.  Furthermore, the block graph itself provides a more
tangible process than before (as this was rather mixed up).

3) Better support for handling pre-/post-conditions.  These are now
turned into WyAL macro blocks.  This reduces a lot of the confusion
related to binding between variables in the code block and the invariant
blocks.  It also means that these macros can be reused between different
verification conditions.  Finally, it improves understanding the generated
WyAL code, as its clearer what is doing what.

There are still some outstanding problems to be resolved, however.  In
particular, the mechanism for handling the typing of variables within
verification conditions needs to be fixed.  This requires an update to
WyCS to support runtime type tests (which should be easy enough).
Furthermore, the algorithm for generating verification conditions from
the block graph is currently quite naive and could be significantly
improved.  Finally, I have added a placeholder where the check for
uninhabitable types should go.  However, this requires extending WyCS to
generate counter examples (I believe).
WyIL: Refactored Assert / Assume bytecodes.

The assert and assume bytecodes were previously not compound bytecodes,
but instead used a target label to signal the end of the assertion /
assumption.  This has now been changed to exploit the new compound
bytecodes.  This means they can contain zero or more bytecodes inside
them.
WyIL: Added Support for Expression Preconditions.

Certain expressions have preconditions.  For example, a division
expression has a precondition that the divisor is non-zero.  This fix
adds proper support in the verification condition generator for
enforcing these preconditions.
TESTING: Added test case for conditionals.

This test case constructs a situation where two paths are joined.  This
tests the joining capability of the verification condition generator.
WyC, WyJC: Added test case While_Valid_44.

This test case tests verification in the presence of break statements.
WyC, WyJC: Added test case DoWhile_Valid_6

This test case does not currently verify, but will in the very near
future.