search

AllanBlanchard / tutoriel_wp

Frama-C and WP tutorial
Other
52 stars 16 forks source link

Question about order3 #42

Closed pdietl closed 1 year ago

pdietl commented 2 years ago

is not https://github.com/AllanBlanchard/tutoriel_wp/blob/f4c1be54e6b2a315836cc125ce7f0ed5f24b2afc/code/function-contract/well-specified/ex-5-order-3-answer.c#L10

implied by https://github.com/AllanBlanchard/tutoriel_wp/blob/f4c1be54e6b2a315836cc125ce7f0ed5f24b2afc/code/function-contract/well-specified/ex-5-order-3-answer.c#L8

AllanBlanchard commented 2 years ago

Indeed, it is. I'll remove the additional property in the next version.

Thanks!

AllanBlanchard commented 1 year ago

Merged in next version