AllanBlanchard / tutoriel_wp

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

/function-contract/behviors/ex-3-triangle-answer.c preconditions fix #21

Closed alexioslyrakis closed 4 years ago

alexioslyrakis commented 4 years ago

Insert preconditions for asserting triangle inequality and that a is the hypotenuse of the triangle. While these were included in the angles_kind() function contact, they were missing from the sides_kind() function contract.

AllanBlanchard commented 4 years ago

In fact, for this particular function, some these preconditions are not necessary.

I'd tend to say that :

  1. 0 <= a && 0 <= b && 0 <= c is absolutely necessary.
  2. a * a <= INT_MAX && b *b <= INT_MAX && c * c <= INT_MAX is unnecessary, so it should be removed
  3. the fact that a is the hypotenuse is unnecessary for this function but as I indicated to specify it, it should be kept

Can you add a commit in this direction? That is to say :

Thank you!

alexioslyrakis commented 4 years ago

Hi Allan, thanks for the feedback, I agree with your comments! I made the required changes, if anything else is needed please let me know.

AllanBlanchard commented 4 years ago

Oh yes, one thing I forgot, just restore the indenting for the functions (2 spaces and not 4), thank you.

Once it is done, I'll merge :)

alexioslyrakis commented 4 years ago

Done :)

AllanBlanchard commented 4 years ago

Thank you!