kmc7468/cs220
1
0
Fork 0
mirror of https://github.com/kmc7468/cs220.git synced 2025-12-14 22:18:46 +00:00
Code Issues Packages Projects Releases Wiki Activity

Add why3 warning for step size.

Browse Source
This commit is contained in:
Jaewoo Kim
2024-10-04 05:11:23 +00:00
parent 8bfbd8f90e
commit b3c36648bf
1 changed files with 1 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
assets/why3/assignment05/README.md
View File

@@ -9,6 +9,7 @@
* You may use [Why3 in your browser](https://www.why3.org/try/). * 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. * 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. * 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. * 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. * To submit your solution, run `./scripts/submit.sh` and submit `assignment05.zip` in the `target` directory to gg.