Lab3 - Maze - Zeilen und Spalten

[JannikV]

Hallo,

im Kommentar der Maze Klasse in Lab3 heißt es

The first number determines the column, the second determines the row.

Jetzt heißt es an einer Stelle im Code und an zwei Stellen in der Aufgabenstellung, dass wir sicherstellen sollen, dass jede Zeile die gleiche Anzahl an Spalten hat.
Natürlich ist das offensichtlich der Fall, denn der erste Array Index gibt ja bereits die Spaltennummer an und damit haben alle Zeilen automatisch maze.length viele Spalten. Was jedoch passieren kann ist, dass nicht alle Spalten gleich viele Zeilen haben

Gehe ich also recht in der Annahme, dass im zitierten Kommentar etwas vertauscht wurde, der erste Index die Zeile und der zweite die Spalte angibt? Dann lässt sich die geforderte Eigenschaft auch wunderbar überprüfen.
...

Wenn ich schon was frage kann ich auch gleich weiter machen: Es ist mit keinem Wort erwähnt, dass wir die Methoden auch implementieren sollen. Das ist aber bestimmt trotzdem gewollt?! Oder?

VG

EDIT: noch ne Frage: wie können wir denn die Syntax überprüfen, also ob wir da sinnvolles JML geschrieben haben? Bisher wurde noch kein Tool und kein Vorgehen diesbezüglich genannt (auch wenn mir klar ist, dass Key das 'irgendwie' kann..)

[hstr]

EDIT: noch ne Frage: wie können wir denn die Syntax überprüfen, also ob wir da sinnvolles JML geschrieben haben? Bisher wurde noch kein Tool und kein Vorgehen diesbezüglich genannt (auch wenn mir klar ist, dass Key das 'irgendwie' kann..)

Also wir haben jetzt herausgefunden das du mit KeY die .java Datei (mit den JML Kommentaren) laden kannst und dann entwickelt KeY irgendeine Formel,
die du dann mit dem automated proof search überprüfen lassen kannst.

VG

[hstr]

Noch eine Frage zum Thema Zeilen und Spalten, hat jemand rausgefunden wie man auf einen Matrixeintrag in JML zugreifen kann?
Denn mit maze[x][y] bekommen wir einen array access Fehler.

VG

[JannikV]

Danke für den Tipp mit Key, damit läufts soweit durch wenn ich die Benutzung des Tools richtig verstanden habe..

Wegen deinem Array Access: Ich greife auch auf maze[x][y] zu und damit funktioniert es ganz gut. Sicher dass es bei euch an der Schreibweise liegt? Ich vermute es sind eher irgendwelche Ranges die nicht stimmen und sowas wie IndexOutOfBounds provozieren? Kann das sein?

VG

[null]

gelöscht

[JannikV]

Öhm, also was du da gepostet hast ist Syntax der Programmiersprache D.

Also ich habe es so gemacht:

Code: Alles auswählen

//@ public invariant x != y;

Wenn ich will dass x ungleich y ist.

Hast aber Recht damit, dass das nicht in der Vorlesung dran kam. Vielleicht kommt das noch. Hoffe mal die werden das durchgehen lassen. Irgendwie muss mans ja machen... und vielleicht ist das ja Teil der nächsten Vorlesung.

VG

EDIT: toll, jetzt hast du deinen Beitrag gelöscht........

[null]

ohh sorry! Ich hatte selbst meinen Fehler bemerkt. Danke aber für deine Antwort. In einem Thread geht es ja auch um Invarianten.

Viele Grüße

[Nathan Wasser]

Hallo,

im Kommentar der Maze Klasse in Lab3 heißt es

The first number determines the column, the second determines the row.

Jetzt heißt es an einer Stelle im Code und an zwei Stellen in der Aufgabenstellung, dass wir sicherstellen sollen, dass jede Zeile die gleiche Anzahl an Spalten hat.
Natürlich ist das offensichtlich der Fall, denn der erste Array Index gibt ja bereits die Spaltennummer an und damit haben alle Zeilen automatisch maze.length viele Spalten. Was jedoch passieren kann ist, dass nicht alle Spalten gleich viele Zeilen haben

Ich erkenne die "Offensichtlichkeit" nicht. Ein Beispiel eines zweidimensionalen Arrays in dem nicht alle Spalten gleich viele Zeilen haben aber dennoch alle Zeilen gleich viele Spalten wäre da eventuell hilfreich.

Wenn ich schon was frage kann ich auch gleich weiter machen: Es ist mit keinem Wort erwähnt, dass wir die Methoden auch implementieren sollen. Das ist aber bestimmt trotzdem gewollt?! Oder?

Nein. Es geht bei der Aufgabe um die Spezifikation mit JML. Wir haben ja mit keinem Wort die Implementierung erwähnt.

[JannikV]

Hallo.

Ich erkenne die "Offensichtlichkeit" nicht. Ein Beispiel eines zweidimensionalen Arrays in dem nicht alle Spalten gleich viele Zeilen haben aber dennoch alle Zeilen gleich viele Spalten wäre da eventuell hilfreich.

Sehr gern.

Code: Alles auswählen

public class Test {
    
    public static void main(String[] args) {
        
        /* - The first number determines the column, the second determines
         * the row. Row and column numbers start at 0.
         */
         
        int[][] a = new int[3][];
        a[0] = new int[42];
        a[1] = new int[666];
        a[2] = new int[1337];
        
        System.out.println("Spaltenanzahl: " + a.length);
        System.out.println("Zeilen in Spalte 0: " + a[0].length);
        System.out.println("Zeilen in Spalte 1: " + a[1].length);
        System.out.println("Zeilen in Spalte 2: " + a[2].length);
        
    }
    
}

Code: Alles auswählen

Spaltenanzahl: 3
Zeilen in Spalte 0: 42
Zeilen in Spalte 1: 666
Zeilen in Spalte 2: 1337

VG

[Nathan Wasser]

Code: Alles auswählen

        int[][] a = new int[3][];
        a[0] = new int[42];
        a[1] = new int[666];
        a[2] = new int[1337];

Zeilen 0 bis 41 haben 3 Spalten, alle weiteren Zeilen haben weniger Spalten. Als Beispiel besteht Zeile 50 aus den beiden Feldern a[1][50] und a[2][50]. Oder gibt es da ein drittes Feld in dieser Zeile welches ich nicht sehe? Somit hat diese Zeile doch wohl auch nur 2 Spalten, oder?

Eventuell hätte ich es auch so formulieren sollen: Zeichne ein zweidimensionales Array mit diesen Eigenschaften.

Das Array hat natürlich offensichtlich a.length viele Einträge, das bestreitet keiner. Jede Zeile muss aber nicht notwendigerweise auch diese Maximalanzahl an Spalten besitzen.

[JannikV]

Ja ok, das kann sein. Da habe ich mich geirrt.
Die Formulierung fand ich an der Stelle etwas verwirrend.
Aber ist es jetzt tatsächlich so, dass der erste Index die Spalte angeben soll?

[Nathan Wasser]

Ja, das soll so sein.

Es ist zwar a[row][col] üblich, aber auch a[x][y], wobei die x-Achse im allgemeinen nach rechts und die y-Achse entweder nach oben oder nach unten. Auch das ist nicht genormt. Somit mag es zwar verwirrend sein, aber darauf muss man sich schon auch gefasst machen; die Verwirrung hört nicht mit dem Universitätsabschluss auf.

[JannikV]

Gut, wenn also das Ziel ist maximale Verwirrung zu stiften, dann wird es beim Cheese Bonus Task wahrscheinlich genau anders rum sein und row ist dort der erste Index?
Quelle Aufgabenstellung: A two-dimensional array field of boolean type cheese indicates the positions of the cheese, e.g. cheese[row][col] is true iff there is a cheese at that position.

VG

[Nathan Wasser]

Gut, wenn also das Ziel ist maximale Verwirrung zu stiften, dann wird es beim Cheese Bonus Task wahrscheinlich genau anders rum sein und row ist dort der erste Index?

Naja, maximale Verwirrung ist schon was anderes.

Das war aber tatsächlich nicht so gewollt, wir werden daher beide Ausrichtungen des cheese-Arrays akzeptieren.