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
Get(Queue)         | Returns a tuple<head, queue - head>

This is my introductory part:

 Queue(Elem :[Undefined -> Elem])

This is my solution for defining operations:

 Operations        |  Output
Create()           -> Queue
Cons(Queue, elem)  -> Queue
Head(Queue)        -> elem
Tail(Queue)        -> Queue
Length(Queue)      -> Integer
Get(Queue)         -> Tuple<Head(Queue), Queue>

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
Head(Create())             = Undefined
Head(Cons(Queue, elem))    = Get(Queue)

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?

  • 1
    $\begingroup$ 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. $\endgroup$ – Derek Elkins left SE Jun 7 '19 at 20:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.