Exercises:

Tutorial

Question 1

As an exercise, change the specification of the class [Polygon]((https://www.openjml.org/tutorial/PolygonMM.java) in the tutorial to enforce the invariant that the longest side should always have a strictly positive value. (Note that 1/2 is 0 in Java.) You may need to use assume statements, as the prover that openjml uses cannot prove some facts about division (due to fundamental limitations on logic). Check your work by using openjml to verify the correctness of the result.

Answer Key

Resources