In sub-directory Examples:

See the examples and their verification conditions in the
following order.

0. swap.txt
1. sequence.txt
2. grades1.txt
3. grades2.txt
4. sum_to_n.txt
5. sigma1.txt
6. isqrt.txt
7. isqrt2.txt
8. prime.txt

Examples with Immutable Arrays

9. array_max.txt
10. array_search.txt
11. binary_search.txt

Examples with Mutable Arrays

12. array_double.txt
13. bubble.txt
14. bubble2.txt

For the examples on Functional Axioms below, you may give the 
axioms to the students and have the students just use them.
They are like "library" functions.

Examples with Functional Axioms

15. fact.txt
16. sigma2.txt
17. gcd.txt
18. prime2.txt

Examples with Lists (polymorphic types)

19. list_length.txt
20. list_reverse.txt

Each file is accompanied by its verification conditions, in a file
<filename>_VCs.txt.