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

In this note we want to present the concept of behavioural categoricity of an abstract data type specification. Intuitively, a specification is behaviourally categoric if it captures the external views the user can have on the data type. More specifically, using this specification, it is possible to prove that two objects are equal if and only if they behave the same, or informally speaking, if and only if they implement the same black box. Providing a general algorithm for proving the behavioural categoricity of any specification is impossible because that algorithm could also decide whether a finite presentation of a group presents the trivial group or not, which Rabin proved to be undecidable. We show by an example of a specification of circular lists that the proof of the categoricity must be done carefully. In this note we want to present the concept of behavioural categoricity of an abstract type specification. Intuitively, a specification is behaviourally categoric if it captures all the external views the user can have on the data type. More specifically, using this specification, it is possible to prove that two objects are equal if and only if they behave the same, or informally speaking, if and only if they implement the same black box. Providing a general algorithm for proving behavioural categoricity of any specification is impossible, because that algorithm could also decide whether a finite presentation of a group presents the trivial group or not, which Rabin proved to be undecidable. We show by an example of a specification of circular lists, that the proof of the categoricity must be done carefully.

Behavioural Categoricity of Abstract Data Type Specifications