From be4fc57edbe7526d35513572a95027deeba311cb Mon Sep 17 00:00:00 2001 From: AnHaechan Date: Tue, 29 Aug 2023 05:28:35 +0000 Subject: [PATCH] why3 assignment: readme --- assets/why3/assignment05/README.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 assets/why3/assignment05/README.md diff --git a/assets/why3/assignment05/README.md b/assets/why3/assignment05/README.md new file mode 100644 index 0000000..245b94f --- /dev/null +++ b/assets/why3/assignment05/README.md @@ -0,0 +1,15 @@ +# 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 `TODO`s in three files: `max.mlw`, `binary_search.mlw`, `pascal.mlw`. + +* You may use [Why3 in your browser](https://why3.lri.fr/try/). + * 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 `TODO`s 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: +* Why3 standard library: