Compile_And_Prove_Demo/examples/strings/example.yaml

name: Strings
description: >
 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.