# Confusion regarding algebraic specification of the queue

I was given the following question in the test where I had to write the algebraic specification and its axioms based on below-defined operations:

 Operations        |  Description
-----------------------------------------------------
Create()           | Brings a queue into existence
Cons(Queue, elem)  | Adds the element to the end of the queue
Head(Queue)        | Returns the element at the front of the queue
Tail(Queue)        | Returns the queue minus its first element
Length(Queue)      | Returns the number of elements in the queue


This is my introductory part:

 Queue(Elem :[Undefined -> Elem])
-----------------------------------------------------
sort<Queue>
import<Integer>
import<Tuple>


This is my solution for defining operations:

 Operations        |  Output
-----------------------------------------------------
Create()           -> Queue
Cons(Queue, elem)  -> Queue
Tail(Queue)        -> Queue
Length(Queue)      -> Integer


I've written operations in terms of inspectors as told by my instructor during the class. So constructors (Create and Cons) * inspector(Head, Tail, Length, Get) = 8 axioms I need to write

Here are my axioms:

 Operations                 |  Axoims
-----------------------------------------------------

Tail(Create())             = Queue
Tail(Cons(Queue, elem))    = elem

Length(Create())           = 0
Length(Cons(Queue, elem))  = |Queue|

Get(Create())              = Tuple<Undefined, Queue>
Get(Cons(Queue, elem))     = If length(queue) == 0 then Tuple<Undefined, Queue> else Tuple<Head(Queue), Queue>


Is my algebraic specification correct according to the given operations table? If not that can be corrected/improved?

• You seem extremely confused. I would suggest talking to a TA or your instructor. It's not clear if you're supposed to be using some system or you're just making up this notation, but either way there's no way for us to know what you mean. Nevertheless, guessing at what you mean, it seems pretty clear that many of the expressions you include don't "type check", don't scope-check, aren't usually allowed in an algebraic specification, or just don't make sense at all. Ignoring those issues, it seems clear that you aren't formalizing the informal specification correctly. – Derek Elkins left SE Jun 7 '19 at 20:41