adding the functional proofs from the overflow branch

contracts/overflow.txt

@@ -4,7 +4,7 @@ de.wiesler.BucketPointers[de.wiesler.BucketPointers::hasRemainingRead(int)].JML
 de.wiesler.BucketPointers[de.wiesler.BucketPointers::increment_write(int)].JML normal_behavior operation contract.0
 de.wiesler.BucketPointers[de.wiesler.BucketPointers::write(int)].JML normal_behavior operation contract.0
 de.wiesler.Buffers[de.wiesler.Buffers::Buffers([I,[I,int)].JML normal_behavior operation contract.0
-# de.wiesler.Buffers[de.wiesler.Buffers::align_to_next_block(int)].JML normal_behavior operation contract.0
+de.wiesler.Buffers[de.wiesler.Buffers::align_to_next_block(int)].JML normal_behavior operation contract.0
 de.wiesler.Buffers[de.wiesler.Buffers::distribute(int,[I,int,int,int,int)].JML normal_behavior operation contract.0
 de.wiesler.Buffers[de.wiesler.Buffers::flush(int,[I,int,int)].JML normal_behavior operation contract.0
 de.wiesler.Buffers[de.wiesler.Buffers::len(int)].JML normal_behavior operation contract.0
@@ -20,7 +20,7 @@ de.wiesler.Classifier[de.wiesler.Classifier::finish_batch([I,[I,int,int,int,int,
 de.wiesler.Classifier[de.wiesler.Classifier::from_sorted_samples([I,[I,int,int)].JML normal_behavior operation contract.0
 de.wiesler.Classifier[de.wiesler.Classifier::num_buckets()].JML normal_behavior operation contract.0
 de.wiesler.Cleanup[de.wiesler.Cleanup::cleanup([I,int,int,de.wiesler.Buffers,[I,de.wiesler.BucketPointers,de.wiesler.Classifier,[I)].JML normal_behavior operation contract.0
-# de.wiesler.Constants[de.wiesler.Constants::log2(int)].JML normal_behavior operation contract.0
+de.wiesler.Constants[de.wiesler.Constants::log2(int)].JML normal_behavior operation contract.0
 de.wiesler.Functions[de.wiesler.Functions::copy_nonoverlapping([I,int,[I,int,int)].JML normal_behavior operation contract.0
 de.wiesler.Functions[de.wiesler.Functions::copy_unique([I,int,int,int,int,[I)].JML normal_behavior operation contract.0
 de.wiesler.Functions[de.wiesler.Functions::fill([I,int,int,int)].JML normal_behavior operation contract.0
@@ -33,11 +33,11 @@ de.wiesler.Partition[de.wiesler.Partition::partition([I,int,int,[I,de.wiesler.Cl
 de.wiesler.Permute[de.wiesler.Permute::permute([I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)].JML normal_behavior operation contract.0
 de.wiesler.Permute[de.wiesler.Permute::place_block(int,[I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)].JML normal_behavior operation contract.0
 de.wiesler.Permute[de.wiesler.Permute::swap_block(int,[I,int,int,de.wiesler.Classifier,de.wiesler.BucketPointers,[I,[I,[I)].JML normal_behavior operation contract.0
-# de.wiesler.SampleParameters[de.wiesler.SampleParameters::SampleParameters(int)].JML normal_behavior operation contract.0
-# de.wiesler.SampleParameters[de.wiesler.SampleParameters::log_buckets(int)].JML normal_behavior operation contract.0
-# de.wiesler.SampleParameters[de.wiesler.SampleParameters::oversampling_factor(int)].JML normal_behavior operation contract.0
-# de.wiesler.Sorter[de.wiesler.Sorter::base_case_sort([I,int,int)].JML normal_behavior operation contract.0
-# de.wiesler.Sorter[de.wiesler.Sorter::fallback_sort([I,int,int)].JML normal_behavior operation contract.0
+de.wiesler.SampleParameters[de.wiesler.SampleParameters::SampleParameters(int)].JML normal_behavior operation contract.0
+de.wiesler.SampleParameters[de.wiesler.SampleParameters::log_buckets(int)].JML normal_behavior operation contract.0
+de.wiesler.SampleParameters[de.wiesler.SampleParameters::oversampling_factor(int)].JML normal_behavior operation contract.0
+de.wiesler.Sorter[de.wiesler.Sorter::base_case_sort([I,int,int)].JML normal_behavior operation contract.0
+de.wiesler.Sorter[de.wiesler.Sorter::fallback_sort([I,int,int)].JML normal_behavior operation contract.0
 de.wiesler.Sorter[de.wiesler.Sorter::partition([I,int,int,[I,de.wiesler.Storage)].JML normal_behavior operation contract.0
 de.wiesler.Sorter[de.wiesler.Sorter::sample([I,int,int,de.wiesler.Storage)].JML normal_behavior operation contract.0
 de.wiesler.Sorter[de.wiesler.Sorter::sample_sort([I,int,int,de.wiesler.Storage)].JML normal_behavior operation contract.0
@@ -48,5 +48,5 @@ de.wiesler.Storage[de.wiesler.Storage::Storage()].JML normal_behavior operation
 de.wiesler.Storage[de.wiesler.Storage::createArray(int)].JML normal_behavior operation contract.0
 de.wiesler.Tree[de.wiesler.Tree::Tree([I,[I,int)].JML normal_behavior operation contract.0
 de.wiesler.Tree[de.wiesler.Tree::build(int,[I,int,int)].JML normal_behavior operation contract.0
-# de.wiesler.Tree[de.wiesler.Tree::classify(int)].JML normal_behavior operation contract.0
-# de.wiesler.Tree[de.wiesler.Tree::classify_all([I,int,int,[I)].JML normal_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::classify(int)].JML normal_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::classify_all([I,int,int,[I)].JML normal_behavior operation contract.0