nullable testexam 1

seepa14
Neuling
Neuling
Beiträge: 9
Registriert: 2. Mai 2013 10:34

nullable testexam 1

Beitrag von seepa14 »

Hallo,

eine Frage zur Aufgabe 6 der Probeklausur 1. Da steht in der Lösung im Java-Code:

protected /*@ spec_public nullable @*/ Interval[] contents = new Interval[1000];


Die Frage ist: Worauf genau bezieht sich das "nullable"? Nur auf die Variable "contents"? Oder nur auf die Werte des Arrays, die laut Aufgabenstellung null sein können?
So wie ich nullable verstanden habe, bezieht es sich auf die Variable. Dann müsste man aber in allen jml contracts noch "requires contents != null" fordern, was aber in der Lösung nicht gemacht wird...


gruß
seepa14

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: nullable testexam 1

Beitrag von Nathan Wasser »

seepa14 hat geschrieben:Die Frage ist: Worauf genau bezieht sich das "nullable"? Nur auf die Variable "contents"? Oder nur auf die Werte des Arrays, die laut Aufgabenstellung null sein können?
Bei Arrays bedeutet "nullable" grundsätzlich beides. Also sowohl das Array selbst, als auch die Elemente des Arrays dürfen null sein.
seepa14 hat geschrieben:Dann müsste man aber in allen jml contracts noch "requires contents != null" fordern, was aber in der Lösung nicht gemacht wird...
Das kann man so lösen, oder wesentlich effizienter eine Invariante einführen, die besagt, dass contents nie null ist. Die Lösungsskizze ist diesbezüglich unvollständig.

xshisdi32
Mausschubser
Mausschubser
Beiträge: 73
Registriert: 10. Apr 2011 17:24
Wohnort: Bessungen, Darmstadt
Kontaktdaten:

Re: nullable testexam 1

Beitrag von xshisdi32 »

Siehe Seite 16 (PDF Seite 25): http://www.eecs.ucf.edu/~leavens/JML/Ol ... refman.pdf (bestätigt Herr Wasser)

seepa14
Neuling
Neuling
Beiträge: 9
Registriert: 2. Mai 2013 10:34

Re: nullable testexam 1

Beitrag von seepa14 »

Danke für die Antworten!

Antworten

Zurück zu „Archiv“