Add examples translated from Java, from the Java Program Verification Challenges

[scuellar]

I've translated examples from

Jacobs, Bart, Joseph Kiniry, and Martijn Warnier. "Java program verification challenges." Formal Methods for Components and Objects: First International Symposium, FMCO 2002, Leiden, The Netherlands, November 5-8, 2002, Revised Lectures 1. Springer Berlin Heidelberg, 2003.

The original examples are in Java, which posed some challenges to translate. Some of the challenges are lost in translation, but nonetheless provide provide semi-realistic examples.

When possible, I tried to replicate the class and inheritance structure from Java to replicate the challenges in C. These created some interesting and complex examples (e.g. java_program_verification_challenges/inprogress/00011_dependen_specifications.c)

Also, because I manually translated these from Java, I was not shy into modifying the code a little to fit CN. A common thing was removing print statements and importing stdio. I still got stuck in half the proofs and a fourth of them crashed/timed-out.

One (rather trivial) example was fully proven and one is still in progress because of it's complexity.

[septract]

Miscategorized examples

• broken/error-proof/00008_overload_dyn_method.c - throws Error 2, should be in broken/error-cerberus

Error:

broken/error-proof/00008_overload_dyn_method.c:42:21: error: feature not yet supported: TODO: Tspec_name, not resolved
    take pv = Owned<Point>(p);
                    ^

• broken/error-timeout/00011_dependen_specifications.c - throws Error 1, should be in broken/error-proof

  broken/error-timeout/00011_dependen_specifications.c:76:5: error: Unprovable constraint
  while (sum <= x)
  ^~~~~~~~~~~~~~~~ 

[scuellar]

@septract recategorized both examples

[septract]

Looks great!