VWP:  Verify with Weakest Preconditions

Installation Files:

    vwp.pl and 
    index1.html

Read "Installation Notes for VWP.pdf" as it cover Windows, MacOS,
and Linux installations.

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. 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
15. partition.txt
16. array_reverse.txt

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

Examples with function calls

21. function_calls.txt
22. function_array_min.txt


(An earlier version, called VC Gen, is also present in this
directory: vcgen.pl.  Its companion html file is index1_vcgen.html.  
If using VC Gen, rename the html file back to index1.html.)