-
Notifications
You must be signed in to change notification settings - Fork 27
Hackeython Working Group: JML Invariant Dialog
Wolfram Pfeifer edited this page Feb 20, 2024
·
3 revisions
Shepard: Richard
Currently, if no loop specification has been annotated using JML annotations in the source code, one can provide one using a specialised instantiation dialog for the loop invariant rule (transformation variant) using JavaDL syntax.
The current situation has the following problems:
- requires JavaDL syntax (and e.g. "false" for "\strictly_nothing" when specifying the loop's assignable clause
- only the loop invariant rule based on transformation is supported
- provided loop specification is not stored ==> proof loading fails
Main Goal Implementation of a suitable (UI, error reporting) dialog for entering loop specifications using JML
Further Objectives
- allow to "override" a present loop invariant
- support for both loop invariant rules (transformation and loop scopes)
- permit saving and loading of proofs where the loop specification has been provided manually