"This is the verification condition generated by WP about our property and our
program, we do need to understand everything here, but we can get the
general idea."
But it should properly be this instead:
"This is the verification condition generated by WP about our property and our
program, we do not need to understand everything here, but we can get the
general idea."
Hi, While reading through your tutorial I spotted a small typo in this section:
https://github.com/AllanBlanchard/tutoriel_wp/blob/25ac4605307f1b12f4a7413dbd71f3e4c6f5cdd2/english/function-contract/contract.tex#LL372-L374C14
Currently it says:
"This is the verification condition generated by WP about our property and our program, we do need to understand everything here, but we can get the general idea."
But it should properly be this instead:
"This is the verification condition generated by WP about our property and our program, we do not need to understand everything here, but we can get the general idea."