English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

class Inconsistent { /*@ normal_behavior @ ensures \result == 0 && @ \result == 1; @*/ /*@ pure @*/ abstract int wrong(); /*@ normal_behavior @ assignable \nothing; @ ensures \result == 6 + wrong() && @ \result == 5 + wrong(); @*/ int bar() { return 6; } } Figure 6: The specification of wrong is not satisfiable. theory used to verify methods that use m in their specification. If this background theory is inconsistent, the reasoning is potentially unsound. For instance, the above axiom is part of the background theory used to verify method bar and allows one to verify bar, although its specification is obviously not satisfiable. Note that this unsoundness occurs even though wrong is not called from bar’s implementation. In practice, unsatisfiable specifications are far less obvious than in the example of method wrong, because they typically involve several normal behavior specification cases including inherited specifications. A verification technique has to ensure that unsatisfiable specifications do not lead to unsound reasoning. To eliminate this source of unsoundness, we use axioms that are weaker than the naive axiomatization above. These axioms require one to prove, by giving a witness, that the specification of a pure method m is satisfiable in order to assume the properties of m and mS. That is, the axioms for m and mS are guarded by the following antecedent: (∃ r, OS ′ • specm(t, p, OS, r, OS ′) ) The existence of a witness has to be proven in order to employ the corresponding axiom. For method wrong, one cannot give a witness r that satisfies r = 0 ∧ r = 1. Therefore, the antecedent of the corresponding axiom is false, and the axiom is void. VOL 05, NO. 5 JOURNAL OF OBJECT TECHNOLOGY 75 REASONING ABOUT METHOD CALLS IN INTERFACE SPECIFICATIONS

Reasoning About Method Calls in Interface Specifications.