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/

Zendy Plus

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

Zendy Tools

Zendy Open

It is proved that in the general case of arbitrary context-free schemes a program is (partially) correct with respect to given initial and final assertions if and only if a suitable finite system of intermediate assertions can be found. Assertions are allowed from the extended state space $\mathcal {V} \times \mathcal {V}$. This result contrasts with the results of [2], where it is proved that if assertions are taken from the original state space $\mathcal {V}$, then in the general case an infinite system of intermediate assertions is needed. The extension of the state space allows a unification in the relational framework of [2], of the (essence of the) results of [2], and of [4], [5] and [6], and provides a semantic counterpart of the use of auxiliary variables.

Completeness with Finite Systems of Intermediate Assertions for Recursive Program Schemes