What is variant for in the invariant configurator? #3273
-
|
Question in title. That field accepts an integer but I am not really sure what it does. I tried to look through the KeY book but haven't found any comment on it. |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment 1 reply
-
|
This field allows you to specify a loop variant, an expression whose value (a) never becomes negative and (b) is strictly decreased in every loop iteration. If you can provide such an expression, then termination of the loop is guaranteed. It is the configurator equivalent of a |
Beta Was this translation helpful? Give feedback.
-
|
Thank you! |
Beta Was this translation helpful? Give feedback.
This field allows you to specify a loop variant, an expression whose value (a) never becomes negative and (b) is strictly decreased in every loop iteration. If you can provide such an expression, then termination of the loop is guaranteed.
It is the configurator equivalent of a
decreasesin JML. You can find that in JML or KeY documentation for comparison,