An Algebraic Dexter-Based Hypertext Reference Model

TL;DR

This paper introduces the first formal algebraic specification of a hypertext reference model based on Dexter, aiming to support hypertext system design and verification.

Contribution

It provides a novel algebraic formalization of the Dexter hypertext model, incorporating updates reflecting hypertext development since the WWW's emergence.

Findings

Formal algebraic specification of hypertext reference model

Supports automatic design process in hypertext systems

Enables logic-based development and verification

Abstract

We present the first formal algebraic specification of a hypertext reference model. It is based on the well-known Dexter Hypertext Reference Model and includes modifications with respect to the development of hypertext since the WWW came up. Our hypertext model was developed as a product model with the aim to automatically support the design process and is extended to a model of hypertext-systems in order to be able to describe the state transitions in this process. While the specification should be easy to read for non-experts in algebraic specification, it guarantees a unique understanding and enables a close connection to logic-based development and verification.