Testexam 1, A6a

tbjoe
Erstie
Erstie
Beiträge: 17
Registriert: 17. Okt 2013 10:27

Testexam 1, A6a

Beitrag von tbjoe »

Hallo,

reicht in der Lösung nicht einfach nur das

Code: Alles auswählen

/*@ public invariant getEnd() >= getStart(); @*/
?
Warum wird spec_public für die privaten Variablen benutzt? Es wird doch auf die public Getter-Methoden zugegriffen.
Warum werden die Getter-Methoden als pure deklariert?

Beides ist denke ich sinnvoll, aber gehört das wirklich zur Lösung dazu?

Xfel
Erstie
Erstie
Beiträge: 14
Registriert: 23. Mär 2013 19:20

Re: Testexam 1, A6a

Beitrag von Xfel »

Naja ich denke entweder man deklariert die felder als spec_public und benutzt sie direkt, oder man deklariert die getter als pure und benutzt die in der Invariante. DIe Verwendung der getter hat den Vorteil, dass die Invariante auch für jede unterklasse gelten muss - wenn man nur die felder verwendet, könnte eine unterklasse die getter überschreiben und verändern...

Antworten

Zurück zu „Archiv“