Program Verification Activity
-----------------------------
0) Setup
	* Install Frama-C
		+ on Ubuntu: sudo apt install frama-c
		+ others: see https://frama-c.com/install-chlorine-20180501.html
			- make sure you also install at least one external prover, e.g. Alt-Ergo or Coq or Why3
	* Open documentation
		+ [WP Plug-in Manual]: https://frama-c.com/download/frama-c-wp-manual.pdf
		+ [WP Tutorial]: https://frama-c.com/download/frama-c-wp-tutorial.pdf
		+ [ACSL By Example]: https://www.cs.umd.edu/class/spring2016/cmsc838G/frama-c/ACSL-by-Example-12.1.0.pdf
		+ [ACSL: ANSI/ISO C Specification Language]: https://frama-c.com/download/acsl.pdf
1) Tutorial
	* Section 1.2 of [WP Plug-in Manual]
	* run wp with:  frama-c -wp <files> -then -report
		+ or a more specific command: frama-c -pp-annot -no-unicode -wp -wp-rte -wp-model Typed+ref -wp-timeout 10 -wp-steps 1000 -wp-coq-timeout 10 <files> -then -report
		+ see pg. 5 of [ACSL: ANSI/ISO C Specification Language]
2) Practice
	* Work though 2-3 examples (or more if you're having fun) in Sections 2--5 of [WP Tutorial] and Sections 3--7 of [ACSL By Example]
		+ there is overlap between them, with the same examples in both
		+ starting with the equal algorithm would be good
3) Apply
	* Use ACSL to formally specify the is_palindrome algorithm
		+ bool is_palindrome(const char* str, unsigned int len) should return true iff str is a palindrome
				- typedef int bool; 
				- #define true 1
				- #define false 0
		+ palindrome := same forward as backwards, e.g. tacocat
		+ all properties must be completely validated
4) [BONUS] Challenge
	* Use ACSL to formally specify the is_palindrome algorithm for Natural numbers (0,1,2,3,...)
		+ bool is_palindrome_nat(unsigned int n)
	* Implement the algorithm
	* Prove correctness with WP
5) Submit
	* tar -czf verification_activity.tgz <files>
		+ e.g. <files> := swap.c swap.h equal.c equal.h is_palindrome.c is_palindrome.h