Algebraic Specification

[AdamBomb89]

I've been trying to wrap my head around algebraic specification lately, and I'm having a rather had time. From what I understand, the idea of algebraic specification is to prove that an ADT is doing what you programmed it to do. For example, a queue should initially be empty, then if two values are enqueued, the first value should be at the front of the queue, and therefor would be the first value dequeued.

But that's about all I understand. Is algebraic specification something I demonstrate in the program itself? I've been reading articles and watched part of a lecture on it on YouTube, and I've gotten an understanding (more or less) of what I need to do, but not exactly how to do it.

Can anyone enlighten me on how to do algebraic specification. Please not, this is not part of a homework assignment, but it's something I've been told I need to understand if I plan to pursue a career in software engineering.

Thanks a lot!

[helios]

the idea of algebraic specification is to prove that an ADT is doing what you programmed it to do.

Not quite. The point of specification is to have a formal definition of a desired behavior. If you push a number into a stack, you want that number to be the next one that will be popped. Once you have an implementation, you can try to prove mathematically if the program actually conforms to that definition.
The specification itself doesn't really have an active part in the proof of correctness. You do need it, but it's part of the proof.

[AdamBomb89]

I've seen some models of algebraic specification that showed essentially what you just said. For example, for a queue, it looked something like this:

isEmpty()
x=5
y=7
push(x)
push(y)
pop() = x

This is also the model I followed in building and testing my queue program.

Or, essentially, x goes into the queue first, and therefore should come out first if the queue is behaving as it should.

So, would it be fair to say the specification is something that's proven by how the program works? For example, if I demonstrate in the queue template I built that when two values are pushed, and then the function to pop is called, the first value pushed is returned, would that constitute proof of correctness? Or is there more to it than that?

[helios]

isEmpty()
x=5
y=7
push(x)
push(y)
pop() = x

Odd. It doesn't actually define any semantics for push, it just exemplifies part of its behavior.
For example, these implementations conform to that specification:

void queue::push(int x){
    if (this->internal!=5)
        this->internal=x;
}

int queue::pop(){
    return this->internal;
}

Something more traditional would be more like

push(this: [Int], value: Int){
    modifies this;
    //The new this is equal to the old one with value prepended to it.
    ensures this == value : pre(this);
}

pop(this: [Int]) = result: Int{
    //this must not be empty.
    requires |this| > 0;
    modifies this;
    //result is the last element of the unmodified this.
    ensures result == pre(this)[|pre(this)| - 1];
    //The new this includes everything in the old one except the last element.
    ensures this ++ [result] == pre(this);
}

So, would it be fair to say the specification is something that's proven by how the program works?

What you prove is not the specification itself. The specification is an arbitrary entity you define. You could specify operations on a queue that behave like random number generators. It's probably not a good idea, but you can do it.
What you prove is whether a given program conforms to some specification.

if I demonstrate in the queue template I built that when two values are pushed, and then the function to pop is called, the first value pushed is returned, would that constitute proof of correctness?

For your example, yes, which is why I argue that the specification is incomplete. There's any number of implementations that don't match one's idea of a queue and yet conform to that specification (unless there's some implicit information I'm unaware of).
For my example, it's a little more complicated. You need to prove that, for any state of the program that meets the preconditions, the functions leave the program in the a state that meets the postconditions.
Note however that mine is an example for formal specification. I'm not sure on the difference between the two.

[AdamBomb89]

My professor never showed us anything like the examples you just gave, so I'm thinking maybe there is some sort of difference between the formal specification you just demonstrated and the algebraic specification he tried to teach us. It's food for thought, though. I'll ask him about it next lab.

http://www.springerlink.com/content/p74x68857786718m/

Toward the bottom of the page in that link, there's an example that's pretty close to what my prof showed us. I've tried to follow his example in the way I build my ADTs.

[helios]

Those look like merely analogues of function signatures. It's like if in my example I had only written

push(this: [Int], value: Int);
pop(this: [Int]): Int;