Simplied Linked List ADT A Linked List is a collection of no

Simplied Linked List ADT

A Linked List is a collection of nodes. The collection allows duplicates. Consider a linked list where each node, of type Node, has two parts:
1. data holds the element, of some generic type Element, stored in the current node, and
2. next holds a reference to the next node in the list.

Let us refer to the sort as LinkedList. An informal description of the operations of the LinkedList is given below:

• create creates an empty linked list.

• add(Element,LinkedList) inserts a new node before the current rst node in the LinkedList with a single element, holding data of type Element and where the second parameter would point to the next node (or null). This operation returns the modied LinkedList.

• isEmpty(LinkedList) returns true if the LinkedList is empty; it returns false otherwise.

• getData(Node) returns Element stored in Node.

• getNext(Node) returns the next node after Node (or null if there is nothing after the current node).

• head(LinkedList) returns the rst node of the LinkedList; null if the list is empty.

• tail(LinkedList) returns the last node of the LinkedList; null if the list is empty.

• size(LinkedList) returns the number of nodes in the LinkedList.

There are 10 axioms in this specication. They correspond to the following rules:
1. The primitive constructor creates an empty linked list.
2. For an empty linked list, head is null.
3. For an empty linked list, tail is null.
4. For a non-empty linked list, head points to the newly constructed node.
5. Adding an element to an empty list creates a linked list with only one element
6. Adding an element to a linked list will increase its size by 1.
7. There is nothing after the tail.
8. For a non-empty linked list, tail points to the last node.
9. For a newly constructed node, data holds the most recently added element.
10. Two nodes, containing elements el2 and el1, respectively, can be successfully linked according to the protocol of the ADT.

Number the axioms in your specication to correspond to the above rules.

Solution

Spec:Linked List(Element);

Sort: List;

Imports:bool,n;

Operations:

create:->linkedlist

add:list*element->linkedlist

head: linkedlist->element

tail:linkedlist*element->bool

size:linkedlist*element->n

Variables:

n:linkedlist

el1 ,el2 :elements

Axioms:

1. isEmpty(create)=true

2.head(create)= undefined

3.add(create ,el)=true

4.head (add(create,el))=el;

5.getData (build(n,el ))=n

6.getNextdata(build( el1,el2))=el2

7.tail(n,el)=true if(getNextdata=undefined)

8.size(n,el)=1+size(el,head(el))