Semantik von assignable und arrays in JML

Jonnylein
Windoof-User
Windoof-User
Beiträge: 30
Registriert: 24. Okt 2007 15:10
Wohnort: Darmstadt

Semantik von assignable und arrays in JML

Beitrag von Jonnylein »

Hallo,

angenommen, ich möchte für eine Methode m, ein array a und einen Integerwert i folgendes festlegen:
  • m verändert den Inhalt von a an der Stelle von i
    m verändert den Wert von i
Da man laut JML Syntax nicht \old in assignable-clauses stehen haben darf, kann ich nicht spezifizieren, dass ich den ursprünglichen Index i (vor Aufruf von m) in meiner assignable-clause verwenden möchte, also wäre folgender Code unzulässig:

Code: Alles auswählen

/*@ assignable i, a[\old(i)] @*/
Wenn ich nun aber folgenden Code verwende, ist nicht klar, ob sich i auf den ALTEN oder den NEUEN Wert i bezieht:

Code: Alles auswählen

/*@ assignable i, a[i] @*/
Was ist denn die genaue Semantik für assignable?

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

Re: Semantik von assignable und arrays in JML

Beitrag von Nathan Wasser »

Siehe Lab 3, Problem 2.

Jonnylein
Windoof-User
Windoof-User
Beiträge: 30
Registriert: 24. Okt 2007 15:10
Wohnort: Darmstadt

Re: Semantik von assignable und arrays in JML

Beitrag von Jonnylein »

Code: Alles auswählen

* Hint: If you use variables for array indices in an assignable-clause,
*       their values are evaluated in the pre-state.
Dementsprechend folgender Code als richtig, um auf das Feld mit pre-state Index zuzugreifen:

Code: Alles auswählen

/*@ assignable i, array[i] @*/ 
Was, wenn ich nun aber nur das Feld des Arrays als assignable deklarieren möchte, das an der Stelle des post-state Index steht? Es ist zwar möglich, den Index als Ausdruck anzugeben, und somit den post-state Index zu errechnen, aber es scheint mir redundant zu sein. Gibt es da andere Möglichkeiten?

Faxe
Erstie
Erstie
Beiträge: 15
Registriert: 3. Jun 2012 13:07

Re: Semantik von assignable und arrays in JML

Beitrag von Faxe »

Moin!

Ich habe auch noch eine Frage zu diesem Thema. Was mich interessiert ist, ob man die Hilfsvariable i die man in dem assignable benutzt noch extra als Integer deklarieren muss.
Was ich meine ist, ist

Code: Alles auswählen

int i;
assignable i, array[i];
nötig?

MfG
Faxe

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

Re: Semantik von assignable und arrays in JML

Beitrag von Nathan Wasser »

Faxe hat geschrieben:Was mich interessiert ist, ob man die Hilfsvariable i die man in dem assignable benutzt noch extra als Integer deklarieren muss.
Was ich meine ist, ist

Code: Alles auswählen

int i;
assignable i, array[i];
nötig?
Ich verstehe die Frage nicht. Soll das beides JML sein? Wie kann eine Variable im Java Code einen Wert zugewisen bekommen ohne vorher deklariert gewesen zu sein? Ist die Variablendeklaration Java und die Assignable-Klausel JML? Ich versteh einfach nicht was hier gefragt wird.

Faxe
Erstie
Erstie
Beiträge: 15
Registriert: 3. Jun 2012 13:07

Re: Semantik von assignable und arrays in JML

Beitrag von Faxe »

Tut mir Leid, dass ich mein Problem so unklar formuliert habe. Das sollte beides JML sein. Aber ich denke ich habe schon ein Lösung für mein Problem. Trotzdem danke, dass du mir helfen wolltest.

Jonnylein
Windoof-User
Windoof-User
Beiträge: 30
Registriert: 24. Okt 2007 15:10
Wohnort: Darmstadt

Re: Semantik von assignable und arrays in JML

Beitrag von Jonnylein »

Faxe hat geschrieben:Moin!

Ich habe auch noch eine Frage zu diesem Thema. Was mich interessiert ist, ob man die Hilfsvariable i die man in dem assignable benutzt noch extra als Integer deklarieren muss.
Was ich meine ist, ist

Code: Alles auswählen

int i;
assignable i, array[i];
nötig?

MfG
Faxe
Wenn i in assignable angegeben wird, muss i vorher deklariert worden sein.
Wenn i außerhalb des Methodenrumpfes deklariert wird, und assignable nicht \everything ist und i durch die Methode verändert wird, muss i in assignable mit angegeben werden.
Wenn i innerhalb des Methodenrumpfes deklariert wird, muss i nicht in assignable angegeben werden.

Ich vermute allerdings, dass dein Verständnis vom Begriff Hilfsvariable hier falsch ist. Es geht zwar nicht aus dem Code-Snippet hervor, aber bei i handelt es sich um ein Feld der Klasse.

Antworten

Zurück zu „Archiv“