Assignment 5: Program correctness and logic

The primary goal of this assignment is to grasp basic concepts about proving a program's correctness with deductive reasoning.
You should fill in TODOs in three files: max.mlw, binary_search.mlw, pascal.mlw.
- You will get PARTIAL SCOREs for each of those three files.
- E.g. If max.mlw and binary_search.mlw get passed, 2 out of 3 points will be given.
You may use Why3 in your browser.
- Clicking Verify button at the top will open a panel on the right side.
- For each task in the panel (e.g. loop invariant preservation), you can right-click it and run the prover.
- Fill in TODOs until the prover can verify all tasks, notified with green check-marks.
To submit your solution, run ./scripts/submit.sh and submit assignment05.zip in the target directory to gg.
More on Why3: https://why3.lri.fr/doc/index.html
Why3 standard library: https://why3.lri.fr/stdlib/index.html