yoogx/spark_examples — pull request #1 by pchapin (2014-08-13 22:42:21+00:00)
Title: The postcondition of Reverse_Array was incorrectly expressed.

I noticed that in Reverse_Array the postcondition needed to reference A'Old. After the fix the postcondition is proved from the loop invariant.