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.
EDIT
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
4
Pre- and postconditions are a contract.
- Precondition is the part of the contract that the caller must meet. If the precondition is not
truethe function must throw an error. - Postcondition is the part of the contract that must be met by the function and describes the expected change to the object/world. If the postcondition is not
truethe implementation has a bug.
Both pre- and postcondition must be boolean expressions.
Let’s take empty? as an example. This function can always be called, so there is not precondition. And the function has no side effect so there is no postcondition.
Let’s take pop as another example. If this function raises an exception on an empty stack the precondition is self.size > 0, on the other hand, if the function returns nil on an empty stack there is no precondition. Both are valid design choices, not familiar with Java’s choice. In either case the postcondition is self.size = previous.size - 1 since the contractual side effect is to remove an element.
And so on …
NB, used pseudo code since not familiar with OCL.