more edits
[cdsspec-compiler.git] / notes / sequential_spec.txt
1 /**
2         This file contains the design thoughts and details about how we use set
3         theory and more formalized way to design a simple specification language to
4         abstractly describe a sequential data structure.
5 */
6
7 1. Design goals:
8    We should design a specification language that users (developers of data
9    structures) can use to describe the specification of sequential data
10    structures. The language should be as mathematical and precise as possible,
11    while it provides enough expressiveness and usability for users. That's to
12    say, users can learn the language easily and take advantage of it to describe
13    as many data structures as possible, e.g, Lock, Queue, Dequeue, LinkedList,
14    Stack, Vector, Hashtable, and UnorderedPool(maybe).
15
16 2. Common data structures:
17    Data structures, to some degree, can be viewed as a collector with specific
18    operation on it. Those operations are done according to the maintained state
19    and pre-defined logic. Set in mathematics has similar characteristics, which
20    contains a collection of elements. However, elements in a set are distint.
21    Order_list, which is a list of elements that have a total order and can
22    duplicate, can be used to complement set. For example, a queue is a container
23    that has a FIFO order on the elements while a stack with a LIFO order. For
24    hashtable, it is a set of pairs (tuples) that has restrictions on the pairs.
25
26 3. Potential constructs:
27    a) Set
28    The set here is conceptually similar to the set in Set Theory. We define our
29    set as a collection of unique and unordered elements. Uniqueness here
30    implicates that the set element should provide an internal equality check.
31    The following is some basic manipulations on set:
32    1) Tuple
33    Every element is an n-dimentional tuple, and each element of a tuple is a
34    tuple. This is basically used to represent the mapping between elements such
35    as a HashMap. Some examples:
36    a or (a) // 1-dimentional tuple, actually any variable is a 1-dimentional tuple
37    (key, value) // 2-dimentional tuple
38    (a, (a, b)) // 2-dimentional tuple, while the second column is a tuple too
39    1-dimentional tuple is the most basic part, it should have a type, such as
40    integer, boolean, or other templated types. The type of a set can be derived
41    from the tuple too. For example, A, B and C are basic types or templated
42    types, we can have Set<(A)>, Set<(A, B)> or Set<(A, (B, C))> as different
43    types. Set<(A)> contains elements of type A, Set<(A, B)> contains tuples of
44    (A, B) and Set<(A, (B, C))> contains tuples of (A, (B, C)). We can get an
45    instance of tuple in a way like (key, value).
46       The tuple has its basic operation dimention(n), which returns the tuple of
47           its nth column.
48    2) Union, intersection, and remove.
49    new_set = union(s1, s2); // returns a new set
50    or
51    s1.union(s2); // s1 becomes the union of s1 and s2, and it returns the new s1
52    It takes two sets and return the union of the two sets. Same for the
53    intersection and complement.
54    3) Cartesian product
55    new_set = prod(s1, s2); // returns the cartisian product of s1 & s2
56    The result of this operation is that a new set of tuples of s1 and s2.
57    4) Remove
58    set.remove(elem);
59    5) Find
60    subset = set.find((key, *)); // use wildcard to find possible subset
61    b) Order_List
62    This is a list of tuples that has an order. It should have the following
63    operations:
64    1) push_back
65    list.push_back(elem);
66    2) push_front
67    list.push_front(elem);
68    3) remove_back
69    elem = list.remove_back();
70    4) remove_front
71    elem = list.remove_front();
72    5) Find
73    elem = list.find(elem);
74    6) IndexOf
75    index = list.indexOf(elem);
76    index = list.indexOf(elem, 1);
77    7) PushAtIndex
78    list.pushAtIndex(1);
79    8) PushAfterElem
80    list.pushAfterElem(target, elem, 10); // find the first matched target from index 10,
81                                          // insert elem after target
82    9) RemoveIfExists
83    RemoveIfExists(elem)
84
85 4. Examples:
86    1) Hashtable
87    @Declare:
88      Set<(Key, Value)> table;
89    @Manipulation:
90      void Put((Key) key, (Value) value) {
91        table.remove(table.find((key, *))).union((key,value));
92          }
93      
94          (Value) Get((Key) key) {
95        return table.find((key, *));
96          }
97
98    2) Stack
99    @Declare:
100      Order_List<(Type)> stack;
101    @Manipulation:
102      void Push((Type) elem) {
103        stack.push_back(elem);
104          }
105
106          (Type) Pop() {
107        return stack.remove_back();
108          }
109
110    3) LinkedList
111    // Suppose we store the pointer and they are unique??
112    @Declare:
113      Order_List<(Type)> list;
114    @Manipulation:
115      void add((Type) target, (Type) elem) {
116        assert(list.find(elem).size() == 1);
117            list.insertAfterElem(target, elem);
118          }
119
120          void remove((Type) target) {
121        list.remove(target);
122          }
123
124    4) UnorderPool
125    // A possible data structure, basically returns an element only once
126    @Declare:
127      Order_List<(Type)> pool;
128    @Manipulation:
129      void insert((Type) elem) {
130        pool.push_back(elem);
131          }
132
133      // Check if elem is possible to be removed; if yes, remove it & return true,
134          // otherwise return false.
135          bool remove((Type) elem) {
136        return pool.removeIfExists(elem);
137          }