Remove Main Methods

[DavePearce]

This provides a detailed report on the current status of all benchmarks:

• 001_average
• 002_fib
• 003_gcd. Ignores strong property about result (e.g. x * y == z)
• 004_matrix
• 006_queens. Ignores strong properties about solutions.
• 007_regex. Ignores strong properties about matching.
• 008_scc. Ignores strong properties about result. Currently this timesout.
• 009_lz77. Ignores strong property decompress(compress(arr)) == arr, but otherwise fine.
• 010_sort. Encountered problem using array::copy and, instead, had to inline copy loop. Potentially, a "lemma" would have done it. Also, doesn't verify deep property that returned array is sorted version of original. That would require some kind of witness or something.
• 011_codejam
• 012_cyclic. The issue here is that of expressivity of Whiley properties.
• 013_btree. Doesn't compile (see Flow Typing Over Type Invariants WhileyCompiler#1095)
• 014_lights
• 015_cashtill
• 016_date. Feels like it should be possible to verify this, though there is a type invariant violation.
• 017_math. Doesn't fully verify as Boogie cannot check specific assertions (e.g. assert max([-37,-71]) == -31) though can check others (e.g. assert max([-45]) == -45) and does verify the body of max() as well.
• 018_heap. Some possible problems with arithmetic ((j-1)/2 >= 0 when j>=0). Big challenge with preservation property as this requires a witness.
• 022_cars
• 023_microwave
• 024_bits. The issue here is that of expressivity of Whiley properties.
• 025_tries
• 026_reverse. The issue here is that of expressivity of Whiley properties.
• 027_c_string. Issue with loop framing.
• 028_flag. Verifies, but doesn't include deep property that result is permutation.
• 029_bipmatch
• 030_fractions
• 032_arrlist. This needs more work!
• 033_bank
• 102_conway (does not compile)
• 104_tictactoe
• 107_minesweeper (does not compile)