wadoon
commented
2 years ago KeY has no support for \lblpos or \lblneg. A \lbl(name, expr) could be useful for the introduction of abbreviation.
KeY has a counter-example mechanism, which can be applied on open proof goals to distinguish whether a goal is non-closeable due to the calculus (semi-decidable) or because of a valid error. The counter-examples mechanism is also exploited for the test case generation, to get input instance for the tests.
mattulbrich
leavens
davidcok
Classic JML includes \lblpos and \lblneg. I suspect these were included because they were used in the encoding into SMT (or the Simplify equivalent) in ancient history. Their function is to report the value of boolean expressions in a counterexample when a proof fails, but only if the value of the expression in the counterexample is true or false, respectively. (Hence they are proof debugging features of the language). They return the value and type of their argument.
0) We could deprecate them from JML because they are proof debugging features, not specification per se. I don't advocate this.
1) I don't think I've ever used \lblpos and \lblneg. What I have used is \lbl, which reports the value of expressions of any type (and independent of their value). I propose \lbl be added to JML. (I would not object to deprecating \lblpos and \lblneg but don't mind retaining them.)
2) The syntax is
(\lblpos <identifier> <expression)(similarly for the others), which is unusual syntax for a programming/specification language. Much more natural would be\lbl(<java-identifier>,<expression>), which can be parsed as a functional form like most other expressions. In this case the<java-identifier>is not in any namespace and does not have a type or value -- it is just used as a label; we could use a string literal for that purpose instead or as well. I advocate adding this syntax (with the identifier or a string literal) and deprecating the old syntax for \lblpos and \lblneg. If we add \lbl we can add just this functional form.3) Even more useful I've found is a
show <expression-list>;statement, which is a specification statement (like assert, etc.). It reports the values of its expressions in the counterexample to a failed proof. It is simpler to insert and remove or comment out of programs than \lbl etc.; the \lbl etc can be used to wrap subexpressions in the method specifications, where show statements cannot be put. I use show all the time in debugging proofs. If we are going to have any common and useful proof assistance features in JML (like clause labels, assume statements), I advocate for this show statement.Writing this makes me realize that I don't know if KeY does anything with counterexamples at all.