VC Generator Code

    vcgen.pl and 
    index1.html

Example of Programs and their Verification Conditions.

See the examples 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

Example with Functional Axioms

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

Example 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.