Strings

This shows basic use of arrays and strings in SPARK, with a rich postcondition quantifying over the content of strings, and a loop invariant stating the same property during loop iteration. In the initial version, the example cannot be proved due to a subtle off-by-one error.