Nachklausur 2014

Benutzeravatar
Informatik Jones
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 14. Aug 2008 07:27

Nachklausur 2014

Beitrag von Informatik Jones »

Hallo,

Ich hätte ein paar Fragen:

Zunächst organisatorisch: Im WS wurde ja gesagt, dass Büchi Automaten nicht in der Klausur drankommen. Ist diese Aussage auch für die Nachklausur gültig?

Zu LTL: Wenn b ein boolean ist. Ist dann []!b (b ist immer falsch) äquivalent zu !(<>b) (es ist nicht wahr, dass b jemals wahr wird).

Eine Frage zur Probeklausur Aufgabe 6b (IntervalSeq): Im Kommentar steht, dass nicht spezifiziert ist an welcher Stelle das neue Intervall eingefügt wird. Ich habe das also (naive?) so verstanden, dass contents unsortiert ist. Sprich es gilt nicht: contents[i-1].getEnd ()<= contents.getStart(). In der MuLö werden aber auch die Elemente nach dem eingefügten Intervall überprüft. Sind diese nicht bereits durch die Invariante abgedeckt? Außerdem weiß man ja, dass das neue Intervall den index i= size hat. Ich wäre spontan in der Klausur so rangegangen:

Code: Alles auswählen

/*@public normal_behavior
@requires size <1000; //contents.length ist ja statisch
@ensures size==\old(size)+1;
@ensures (\forall int i; i < \old(size); contents[i] == \old(contents[i]));
@ensures contents[\old(size)]==iv;
@assignable contents, contents[*], size;
@
@also 
@...
@*/

Wäre das OK so, oder ist hier eine allgemeinere Lösung gefragt, obwohl die Werte bekannt sind?

Eine Frage zur letzten Klausur im WS : Ich konnte leider wegen Krankheit nicht mitschreiben. Mich würde interessieren in wie weit die Probeklausuren vom Umfang und der Schwierigkeit der Klausur repräsentieren.

Vielen Dank im Voraus!

LG,

Andre

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

Re: Nachklausur 2014

Beitrag von Nathan Wasser »

Es wird bei der Nachklausur nichts drankommen, was nicht auch bei der Klausur im Herbst hätte drankommen können.

Natürlich ist []!b äquivalent zu !<>b.

Wenn etwas nicht spezifiziert ist, so darf die Implementierung frei gewählt werden. Nicht jedoch die Spezifikation, denn, naja, es sollte nicht spezifiziert werden. Wenn die Variable "x" positiv sein soll, aber weiter nicht spezifiziert, dann darf man nicht spezifizieren, dass "x" immer 5 ist. Wenn es aber bei einer Implementierung so ist, dass "x" immer den Wert 5 hat, dann entspricht es der Spezifikation. Auch den festen Wert 1000 zu nehmen ist nicht in Ordnung. Eine andere Methode könnte ja zum Beispiel "contents = new Interval[1001];" beinhalten.

Zur letzten Frage können vielleicht Kommilitonen eine bessere Antwort liefern.

Antworten

Zurück zu „Archiv“