The Formal Design Model of Doubly-Linked-Circular Lists (DLC-Lists)

1. Introduction

Data object modeling is a process to creatively extract and abstractly represent a real-world problem by data models. A list is a finite sequence of elements where the order information of its elements is preserved beyond that of sets (Stubbs & Webre, 1985; McDermid, 1991; Bollella et al., 2002). Many important data objects can be modeled and implemented by lists such as a set of data with keys, a sentence for natural language parsing, a sequential file, a tree, and a graph (Wiener and Pinson, 2000).

A list can be formally modeled by an Abstract Data Type (ADT) (Guttag, 1977; Broy et al., 1984; Cardelli & Wegner, 1985; Stubbs & Webre, 1985), which is an abstract logical model of a complex and/or user defined data structure with a set of predefined operations. Using types to model real-world entities can be traced back to the mathematical thought of Bertrand Russell in1900s (Russell, 1903) and Georg Cantor in 1932 (Lipschutz & Lipson, 1997). A number of ADTs have been identified in computing and system modeling such as stack, queue, sequence, record, array, list, tree, file, and graph (Broy et al., 1984; Mitchell, 1990; McDermid, 1991; Wang, 2007; Wang, Ngolah, Tan, Tian, & Sheu, 2010). ADTs possess the following properties: (1) An extension of type constructions by integrating both data structures and functional behaviors; (2) A hybrid data object modeling technique that encapsulates both user defined data structures and allowable operations on them; (3) The interface and implementation of an ADT are separated where detailed implementation of the ADT is hidden to applications that invoke the ADT and its predefined operations.

In order to formally model the list ADT, an expressive denotational mathematics, Real-Time Process Algebra (RTPA) (Wang, 2002, 2007, 2008a, 2008b, 2008c, 2008d; Wang, Tan, & Ngolah, 2010), is adopted, which allows both architectural and behavioral models of lists to be rigorously designed and implemented in a top-down approach. According to the RTPA methodology for system modeling and refinement, a formal list can be rigorously modeled using two fundamental techniques known as the unified data models and the unified process models (Wang, 2007).

• Definition 1: A Unified Data Model (UDM) is a generic architectural model for a software system, its internal control structures, and its interfaces with hardware components, which can be rigorously modeled and refined as an n-tuple, i.e.:

  
  (1)

where S_i, 1 ≤ i ≤ n, is a set and also a type of elements e that share the property p_i,.

• Definition 2: The Unified Process Model (UPM) of a program ℘ is a composition of a finite set of m processes according to the time-, event-, and interrupt-based process dispatching rules,, i.e.:

  
  (2)

where s_i and s_j are one of the 17 RTPA meta-processes, r_ij is one of the 17 RTPA algebraic process operations, and e_k is a general, timing, or interrupt event.