Post Conditions für InsertAt und remove

[Rahim]

Ich kriege es nicht hin post conditions für InsertAt und remove zu definieren. Ich hatte bei append einen guten Ansatz der klappt aber ich kann das nicht auf die anderen beiden übertragen. Hat jemand Tipps wie ich die 2 post conditions machen sollte? Hier mein Code bis jetzt

model List

class List
  attributes
    elements:Sequence(OclAny)

  operations
    append(element:OclAny)
   
    remove(index:Integer)
   
    insertAt(element:OclAny, index:Integer)
   
    size():Integer =
      self.elements->size()
   
    indexOf(element:OclAny) : Integer =
      self.elements->asSequence()->indexOf(element)
end

constraints

context List::append(element:OclAny)
  post itemAdded:
    self.size@pre() + 1 = self.size()
  post itemIsLast:
    self.elements->at(self.elements->size()) = element

 

[krgewb]

Bitte immer in code-Tags posten.