Skip to content

Commit

Permalink
Add why3 warning for step size.
Browse files Browse the repository at this point in the history
  • Loading branch information
Jaewoo Kim committed Oct 4, 2024
1 parent 8bfbd8f commit b3c3664
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions assets/why3/assignment05/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
* You may use [Why3 in your browser](https://www.why3.org/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.
* Important: The prover might not be able to verify the correct solution if the number of steps is too small. Make sure to test with 1000~5000 steps.
* 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.
Expand Down

0 comments on commit b3c3664

Please sign in to comment.