Lab3 - Maze - Zeilen und Spalten

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Lab3 - Maze - Zeilen und Spalten

Beitrag von 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 :roll:

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? :P

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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von hstr »

JannikV hat geschrieben: 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
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 128
Registriert: 14. Apr 2011 22:52

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von null »

gelöscht

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 168
Registriert: 21. Apr 2012 14:58

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von Nathan Wasser »

JannikV hat geschrieben: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 :roll:
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? :P
Nein. Es geht bei der Aufgabe um die Spezifikation mit JML. Wir haben ja mit keinem Wort die Implementierung erwähnt.

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von JannikV »

Hallo.
Nathan Wasser hat geschrieben: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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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.

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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. :)

Benutzeravatar
JannikV
Nerd
Nerd
Beiträge: 609
Registriert: 24. Apr 2011 12:42

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von 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
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

Re: Lab3 - Maze - Zeilen und Spalten

Beitrag von Nathan Wasser »

JannikV hat geschrieben: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.

Antworten

Zurück zu „Archiv“