Lösungsversuch
Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
OCL Braindump 2010/11
Hey,
da ich bei dem Thema OCL bisher immernoch ein wenig auf dem Schlauch stehe (v.a. mit der Navigation), stell ich hier mal meine Versuche für den Braindump 2010/11 rein. Braindump gibts hier.
a)
context: Termin
inv: Semesterwoche <= 15 and Semesterwoche >= 1
b)
context: Vortrag
inv: self.allInstances → size() <= 20
c)
context: Termin
inv: self.Vortrag → size() <= 3
d) 2 Möglichkeiten (ich weiß es gibt viele)
context: Termin
inv: self.Vortrag → collect (Themengebiet) → asSet() → size() = 1
oder
inv: self.Vortrag → forAll (v1, v2 | v1.Themengebiet <> v2.Themengebiet)
e)
context: Vortrag
inv: self.Referent.Betreuer.Forschungsgebiet → exists(self.Themengebiet)
f)
context: Termin::delVortrag(title : string)
pre: self.Vortrag.title → includes(title)
post: self.Vortrag → size() +1 = self.Vortrag@pre → size() // wo setzt man genau das @pre rein? Würde das so funktionieren?
g)
context: Vortrag
inv: self.allInstances.title → forAll(t1,t2 | t1 <> t2)
Bitte verbessert mich, falls etwas falsch ist.
inv: allInstances()->size() <= 20 - Klammern nicht vergessen!
collect() kannte ich noch nicht, aber wenn das so funktioniert sieht das elegant aus. Gibt es für Bags die Operation size() nicht oder warum das „asSet()“?
Bei deiner zweiten Lösung hast du sicher „=“ statt „<>“ gemeint.
Würde ich so unterschreiben, wenn da „includes“ statt „exists“ stehen würde. Mit exists würde es aber auch gehen:
… → exists(t:Themengebiet | t = self.themengebiet)
Du hast noch vergessen, sicherzustellen, dass der Vortrag danach auch wirklich gelöscht ist. Außerdem denke ich, dass deine Precondition so falsch ist (wenn das eine korrekte Kurzschreibweise ist, dann korrigiert mich bitte).
context Termin::delVortrag(title: string)
pre: vortraege->exists(v:Vortrag|v.titel=title)
post: vortraege->forAll(v:Vortrag|v.titel <> title) and vortraege->size() = vortraege@pre->size() - 1
Denk daran, dass „self“ bei allInstances auch mit dabei ist.
context Vortrag
inv: not Vortrag.allInstances()->exists(v:Vortrag|(v <> self) and (v.titel = self.titel))
oder
inv: Vortrag.allInstances() → forAll(v1,v2 | (v1 <> v2) implies (v1.titel <> v2.titel))
oder
inv: Vortrag.allInstances() → select(v:Vortrag| v.titel = self.titel)->size()=1
Vielen Dank.
zu d)
collect sammelt auch alle doppelten Werte zusammen. Mit asSet() werden die doppelten Werte rausgeworfen.
Ja, ich meinte “=”. Da bin ich wohl in die falsche Zeile geraten.
zu e)
Meins sollte auch richtig sein.
zu f)
Ich sollte auf meinen Blättern nicht so rumschmieren 
Ich habe:
self.Vortrag.title → excludes(title)
Man kann hier einfach ‘title’ schreiben, weils ein Argument der Funktion ist. In der Klausur werd ich aber sicherheitshalber alles ausschreiben.
Soweit ich weiß kann man aber vieles weglassen, wenn man sich Schreibarbeit ersparen will. Natürlich auf Kosten der Lesbarkeit.
zu g)
Danke, das hatte ich ganz übersehen.