Skip to content

Hackeython Working Group: JML Invariant Dialog

Wolfram Pfeifer edited this page Feb 20, 2024 · 3 revisions

Shepard: Richard

Motivation

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

Goal

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