I have an exam coming up and I'm looking at past papers to get some ideas of what to expect. I'm a bit stuck on the following one and would really appreciate if someone could give some example answers.
Write preconditions and postconditions in OCL for each of the following operations (included in the Stack class in the java.util package):
- (1) Boolean empty() - Tests if this stack is empty
- (2) E peek() - Looks at the object at the top of this stack without removing from the stack
- (3) E pop() - Removes the object at the top of this stack and returns that object as the value of this operation
- (4) E push(E item) - pushes an item onto the top of this stack
Here E denotes the type of elements in the stack.
My attempts are as follows:
Boolean empty() pre: none post: self -> IsEmpty() = true //should this be result -> IsEmpty() = true because it returns a boolean value? E peek() pre: self -> NotEmpty() = true post: result = ??? // I lose hope at this stage.
I also don't know if I should be referencing the elements in the stack. For example: self.elements -> IsEmpty() = true
If anyone could help me out I'd really appreciate it.
A friend has the following ideas:
context Stack empty() pre: self.data.size = 0 context Stack peek() pre: self.data.AsSequence.first context Stack pop() pre: !self.data.isEmpty post: self.data.AsSequence.first.remove (not sure about this one) post: self.data.count = @pre:data - 1 context Stack push(E Item) post: self.data.asSquence.prepend(E.asSequence) post: self.data.size = @pre.data.size + 1