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

A recent trend in object oriented (OO) programming languages is the use ofAccess Permissions (APs) as an abstraction for controlling concurrentexecutions of programs. The use of AP source code annotations defines aprotocol specifying how object references can access the mutable state ofobjects. Although the use of APs simplifies the task of writing concurrentcode, an unsystematic use of them can lead to subtle problems. This paperpresents a declarative interpretation of APs as Linear Concurrent ConstraintPrograms (lcc). We represent APs as constraints (i.e., formulas in logic) in anunderlying constraint system whose entailment relation models thetransformation rules of APs. Moreover, we use processes in lcc to model thedependencies imposed by APs, thus allowing the faithful representation of theirflow in the program. We verify relevant properties about AP programs by takingadvantage of the interpretation of lcc processes as formulas in Girard'sintuitionistic linear logic (ILL). Properties include deadlock detection,program correctness (whether programs adhere to their AP specifications ornot), and the ability of methods to run concurrently. By relying on a focusingdiscipline for ILL, we provide a complexity measure for proofs of the abovementioned properties. The effectiveness of our verification techniques isdemonstrated by implementing the Alcove tool that includes an animator and averifier. The former executes the lcc model, observing the flow of APs andquickly finding inconsistencies of the APs vis-a-vis the implementation. Thelatter is an automatic theorem prover based on ILL. This paper is underconsideration for publication in Theory and Practice of Logic Programming(TPLP).

A Concurrent Constraint Programming Interpretation of Access Permissions