Axiom

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Axiom
Ich habe noch nicht ganz verstanden, wie man ein Axiom selber schreibt oder auch wie man es liest.
Das ist mir auch aus den Übungs- und Forlesungsfolien nicht ganz klar geworden und im Internet findet man irgendwie auch nichts dazu.
Könnte mir das jemand nochmal erklären oder hat jemand eine gute Quelle für mich?


Altklasuren und deren Lösungen

Beachte: Die Lösungen sind von Studenten für Studenten erstellt (also keine Garantie auf Korrektheit).


Tja, leider ist die Erklärung auch relativ dürftig.
Aber zuerst mal: Was willst du eigentlich mit einem abstrakten Datentyp tun, wozu ist der da, usw.?

Ein ADT ist letztlich nichts anderes als eine Klasse von Objekten, die “nur” durch die Operationen, sowie deren Funktionalitäten, die dieser ADT besitzt, definiert ist.
Die Definition besteht hierbei nur aus den syntaktischen und semantischen Eigenschaften, die diese Operationen besitzen. Diese Beschreibung sagt aber nur aus, WAS diese Methoden können sollen, nicht hingegen, WIE sie es können sollen. Der Zugriff erfolgt ausschließlich über die definierten Schnittstellen.

Damit kommen wir zum Aufbau der Definition eines ADTs:

Zuerst wird der adt benannt, also z.B.

adt stack

Dann folgen die Datentypen, die verwendet werden.

z.B. Boolean, T, was-auch-immer.

Dann folgt die Liste der Operationen, kurz ops, die verwendet wird, welche Parameter verwendet werden und was die Methode zurück gibt.

z.B.
ops
emptyStack: → STACK // erzeuge leeren Stack



.

Bei mehreren Parametern wird einfach ein X dazwischen gesetzt:

push: ELEMENT × STACK → STACK (Legt ein Element auf den Stack drauf)

D.h. hier sind als Parameter ein Stack sowie ein Element vorgegeben. Es wird ein Stack zurückgegeben.

Kommen wir nun zum eigentlich spannenden Teil, der Semantik:

Hierbei beschreiben wir - wie oben gesagt - nur ALLGEMEIN GÜLTIGE Regeln, nach denen diese ADTs funktionieren.

z.B. - um beim Stack zu bleiben:

ops:
emptyStack: → STACK // erzeuge leeren Stack
isEmptyStack: STACK → Boolean // überprüft ob Stack leer ist, gibt Boolean zurück.
push: ELEMENT × STACK → STACK // Legt neues Element auf den Stapel und gibt Stapel zurück.

axs:
x: ELEMENT
s: STACK
(Anmerkung von mir: Das sind nur zwei spezifizierte Parameter, die zur Verwendung für die Definition der axs gedacht sind, mehr nicht.)

isStackEmpty(emptyStack()) = TRUE // Logisch, denn ein leerer erzeugter Stack ist IMMER leer. Könnte man auch als “Basisfall” bezeichnen.
isStackEmpty(Push(x,s)) = FALSE // Auch relativ ersichtlich: Die Methode Push legt ein neues Element auf den Stapel. Selbst wenn wir hierbei ein neues “Emptystack” erzeugen und als zweiten Parameter nehmen, ändert das nichts an dem Wahrheitsgehalt dieser Aussage. d.H. diese Aussage über die Funktionalität gilt IMMER.

end Stack

Das ist auch unser Ziel: Wir wollen, wie gesagt, ALLGEMEIN GÜLTIGE Aussagen über die Verhaltensweisen treffen.

Das war jetzt nen simples Beispiel aus Wikipedia, kommen wir mal zu einem “nicht trivialen” Beispielen aus einer AUD-Klausur: (Anmerkung: Das ist meine persönliche Lösung, keine Garantie auf Richtigkeit, allerdings soll das auch nur als Beispiel dienen, wie sowas aussehen könnte.)

In der SS-2016-Klausur, Aufgabe 5, ist nach der Definition eines “Langtons Ameise”-ADT gefragt. Die Beschreibung kannst du dir durchlesen, hierbei gehe ich mal auf Aufgabe a) ein:
adt LA
sorts LA, boolean, int
ops:
New: int 7→ LA // startet Ameise auf neuem Raster in ubergebener Richtung ¨ d
Step: LA 7→ LA // Ameise macht einen Schritt nach obigen Regeln
getCol: LA × int × int 7→ boolean // liefert die aktuelle Farbe im ubergebenen Feld ¨ (x, y)
getDir: LA 7→ int // liefert die aktuelle Ausrichtung d der Ameise
getX: LA 7→ int // liefert die aktuelle x-Koordinate der Ameise
getY: LA 7→ int // liefert die aktuelle y-Koordinate der Ameise

axs:
getCol(New(d), x, y) = false

Gefragt ist nun nach dem Axiom zu: getCol(Step(l), x, y).

Hierzu einige Erklärungen:

Übergeben ist uns als Parameter nicht etwa eine Ameise, sondern eine Methode mit einer Ameise, die eine Ameise als Parameter zurückgibt. Auch gibt es hierbei (Aus der Aufgabenstellung a ersichtlich) eine einfache Fallunterscheidung. d.H. das Axiom, das wir haben wollen, muss die Eigenschaft der Step-Methode beinhalten UND dazu noch eine Fallunterscheidung beinhalten.
Das mag erst mal hart klingen, ist es aber bei genauerer Betrachtung nicht wirklich, denn: Alles was wir haben wollen ist eine ALLGEMEIN GÜLTIGE Regel.
Dazu: Die Step-Methode funktioniert immer so:
Ändere die Richtung, basierend auf der Farbe.
Wechsle Farbe des Feldes.
Gehe einen Schritt weiter.

Daraus folgt:

getCol(Step(l), x, y) = getCol(l, l.getX(), l.getY()), falls (getCol(Step(Step(l)), l.getX(), l.getY()) UND getCol(l, l.getX(), l.getY))XOR (!getCol(Step(Step(l)), Step(Step(l)).getX(), Step(Step(l)).getY()) UND !getCol(l, l.getX(), l.getY))
// Hier wird simuliert, das dieses Feld schon einmal besucht wurde. d.H. Die Farbe des Feldes entspricht der Farbe des Feldes vor dem STEP, ver-UND-et mit der Farbe des Feldes nach dem nächsten Step. Beide mit ihrer Negation ver-XOR-t, da nur eines von Beidem gelten soll. So meine Überlegung.

getCol(Step(l), x, y) = !getCol(l, l.getX(), l.getY() sonst. // Basisfall, Ameise ändert das Feld, auf das sie als nächstes tritt NACH dem Step. Was also heißt, dass sonst immer die Farbe des Feldes nach dem Step das Gegenteil der Farbe des Feldes vor dem Step ist.

Gehen wir mal zur b: Hierbei soll die getDir als Axiom beschrieben werden. GetDir liefert die aktuelle Ausrichtung zurück. Diese ist - wie bereits gesehen - von der Farbe des AKTUELLEN Feldes abhängig. d.H. hier muss auf jedem Fall GetCol in irgendeiner Art vorkommen. Was hier aber eigentlich gefragt wird: Wie du mit der Linksdrehung bei einem Step bzw. der Rechtsdrehung bei einem Step verfährst und was das genau für die Direction bedeutet. Auch hierbei gibt es - wieder - einen allgemeinen Fall und einen “speziellen” Fall.

getDir(New(d)) = d // Trivialfall, ist auch so in der Aufgabe vorgegeben.

getDir(Step(l)) = (getDir(l)+1)%4
falls (getCol(l, l.getX(), l.getY()) UND FALSE) AND getCol(Step(l), Step(l.getX(), Step(l.getY()) // Hier wieder: Du triffst von einem weißen auf ein schwarzes Feld, hierbei ist eine Drehung nach links gefragt. Die Drehung nach links ist sehr einfach zu beschreiben, wohingegen die Bedingung, unter der das geschieht, die eigentliche Schwierigkeit darstellt. Dazu muss Folgendes gelten: Das Feld, auf dem du dich jetzt befindest, muss weiß sein, das Folgefeld (Mit dem Step) schwarz. Da hier keine == Vergleichs-Operatoren erlaubt sind, bedient man sich eines Tricks: Du ver-UNDest das Ergebnis von COL mit False, stellst somit sicher, dass das nur dann wahr ist, wenn beide falsch sind (Dementsprechend das vorherige Feld weiß ist), und das nachfolgende Feld schwarz.

getDir(Step(l)) = (getDir(l)+3)%4 sonst // Wieder relativ trivial

Ich hoffe, ich habe das hier einigermaßen richtig gelöst (Habe mich heute mal zur Auffrischung dran gesetzt), es wäre aber nett, wenn jemand das überprüfen könnte, was ich geschrieben habe, vor allem würde es mich interessieren, ob meine Gedankengänge bzgl. letzter Aufgabe richtig waren bzw. sind.


Oh, viiiielen Dank für die ausführliche Antwort :slight_smile:
Ich werde mich da gleich mal ransetzen.
Finde es trotzdem irgendwie … na ja… dass es nirgends richtig ausführlich erklärt ist (auch nicht im Netz) und davon trotzdem unsere Einzelpunkte abhängen!


Ok, also so, wie ich es verstanden habe, schreibt man ein Axiom so:

namederMethode(übergebenerParameter1, übergebenerParameter2) = RueckgabeParameter

oder:

namederMethode(benutzteMethode1(ParameterFuerDieMethode1, ParameterFuerDieMethode2), benutzteMethode2(ParameterFuerDieMethode1, ParameterFuerDieMethode2)) = if Parameter == bla, dann Rueckgabewert1, else RueckgabeWert2

Ist das von der Struktur her richtig?

Und wenn man nicht weiß, wie man die Parameter nennen soll, soll man die dann einfach irgendwie nennen?


[quote=Caroline]
Ist das von der Struktur her richtig?

Und wenn man nicht weiß, wie man die Parameter nennen soll, soll man die dann einfach irgendwie nennen?[/quote]
Zwei Mal Ja :slight_smile:

Die Struktur kann beliebig kompliziert werden, entscheidend ist, dass du alle Fälle berücksichtigst. Stell dir jeden möglichen Methodenaufruf vor und versuche für diesen eines der Axiome zu finden, das passt. Findest du keins, hast du einen Fall übersehen. Findest du mehr als eins und deren Ausgaben widersprechen sich, hast du ein inkonsistentes Axiomensystem, musst das also auch korrigieren.


Yo genau, das ist eigentlich auch schon alles. Kann dir nur empfehlen, das an den ganzen Altklausuren zu üben (am besten ohne nachzuschauen). Und wenn du davon so ziemlich alle Beispiele kannst und verstanden hast, dann haste auch ne gute Chance auf ne gute Punktzahl zumindest, sollte dieser Themenbereich in der Klausur drankommen :slight_smile:


Hey ich hab eine Frage zu der Aufgabe, weil ich da überhaupt nicht weiterkomm, aber zunächst @Zeilenknecht, hälst du noch an der obigen Lösung fest oder hast dir schon dazu was neues überlegt?

Mein Grundlegendes Problem bezieht sich auf die Parameter:
getCol(Step(Ameise), x, y)= getCol(Ameise, Ameise.getX(), Ameise.getY())

  • Repräsentiert der Parameter Ameise den Zustand der Ameise vor dem Step(), Also hätte Step(Ameise) eine andere Objektbezeichnung, sagen wir Ameise1.1 ?

Daneben würde ich gerne die Lösungidee zu a) kurz verbal besprechen:


Tja, und hier bin ich raus. Weil für mich ist es entweder true, wenn getCol((Step(l), Step(l).get(x), Step(l).get(Y) ) true ist und ansonsten false.


Ich habe mir schon länger etwas anderes überlegt, wollte aber wissen, ob auch nur irgendjemanden meine beiden dicken Denkfehler aufgefallen sind.

Das war auch mein 1. Denkfehler: x und y sind „irgendwelche“ Zahlen, sie müssen nicht mal deckungsgleich sein mit l.getX() und l.getY(). Ich hatte aber genau das angenommen.

Ja, das war mein 2. Denkfehler. Ich dachte, man müsse das wissen - tut man aber nicht!
Was macht GetCol genau? Sie fragt ab, ob bei dem Feld an der Stelle x,y false oder true steht - sonst nichts.

Das Grid ist immer anfänglich als False initialisiert. Eine qualitative Hypothese in Richtung „Sonst false“ wäre also durchaus angebracht. Wann ist der Eintrag aber True?
Eigentlich nur unter drei Bedingungen, wovon zwei gleichzeitig gelten müssen und eine andere auch auftreten kann.
1.) x und y müssen l.getX() und l.getY() entsprechen.
2.) getCol(l, x, y) muss false sein.

ODER:

3.) getCol(l, x, y) ist true.

Daraus folgt: GetCol(Step(l), x y ) = true, falls ((x==l.getX()&& y==l.getY() &&!getCol(l,x,y)) OR (getCol(l,x,y))

Wichtige Anmerkung hierzu:

Ich weiß nicht, ob ein Vergleich mittels == erlaubt ist, allerdings wird auch nicht explizit erwähnt, das solche Operatoren nicht erlaubt sind, was ja in Altklausuren auch genau so drin stand, weswegen ich nur davon ausgehen kann, dass das, was ich hier stehen habe, vorausgesetzt ich habe wieder keinen dicken Denkfehler drin, richtig ist.

Ich hoffe aber ich konnte wenigstens etwas Licht in die Sache bringen.

1 „Gefällt mir“

Danke für die Erläuterung, da muss ich mir jetzt auch noch mal genauer gedanken zu machen aber, aber vorab hätt ich auf die schnelle eine Frage zu dem was mir aufällt:

Warum muss getCol(l, x, y) false sein, damit getCol(Step(l), x, y) true ist? Das würde doch bedeuten, dass man von der Farbe des Feldes von dem die Ameise kommt, auf die Farbe des Feldes auf das sie geht, schließen kann.

Aber führt man das Beispiel in der Klausur weiter, dann macht die Ameise den nächsten Schritt wieder auf Start, dreht sich nach links und geht hier von einem schwarzen → auf ein weißes Feld. Also die Aussage stimmt nur in den meisten, aber nicht in allen Fällen:
Schritt 1- 3: Weiß → Weiß;
Schritt 4: Weiß → Schwarz
Schritt 5: Schwarz → Weiß

Wenn es True oder False sein kann, ist es dann nicht irrelevant für die argumentation?

Falls ich irgendwie auf dem Schlauch stehe, entschuldige ich mich schon mal vorab. Aber bei adt fehlt mir noch der „klick“. Nebenbeibemerkt, ich denke die überprüfung mit == sollte nach dem was ich bisher so gesehen habe klar gehen.


Es sind zwei Bedingungen, du vergisst die Zweite: Das vorige Feld muss weiß (false) gefärbt sein, damit es schwarz (true) gefärbt werden kann.
Das zusammen mit der Bedingung, das die abgefragten Koordinaten denen entsprechen, auf denen sich die Ameise vorher befand (also auf denen der Step ausgeführt wird) sind doch die Bedingungen, nach denen eine Schwarz-Färbung simuliert wird.

Lies dir erst mal die Happens-Ordnung bei der Methode durch:
Drehe dich je nach Farbe
Färbe das JETZIGE Feld
Gehe einen Schritt weiter.

Da steht nichts davon, dass das Feld nach dem Step gefärbt werden soll.

Die erste Bedingung der beiden gilt nur mit den anderen Bedingungen, die Zweite hingegen alleine.
z.B: Step wird ausgeführt, aber betrifft das Feld nicht, das Feld wurde aber (was-weiß-ich-wie-viele) Züge vorher schon mal schwarz gefärbt.


Angenommen:
Feld(x,y) ist weiß(False):
x = l.getX(), y= l.getY();

step => Feld(x,y) = True(Schwarz).

GetCol(Step(l), x, y) = true, falls(…) das stimmt.

Jetzt selbe Annahme, aber Feld(x, y) ist schwarz(True):

step => Feld(x,y) =False(Feld nach dem step weiß)
GetCol(Step(l), x, y) =true, falls getCol(l, x, y) // gib jetzt True zurück, obwohl das Feld False ist.

somit wäre noch ein Fall abzudecken.

Daraus folgt: GetCol(Step(l), x, y ) = true,
falls ((x==l.getX()&& y==l.getY() &&!getCol(l,x,y)) OR (getCol(l,x,y)&& (x!=l.getX() OR y!=l.getY())).

Und noch zum zweiten GetCol, das mit dem sonst dahinter. Ich würde einfach „GetCol(Step(l), x, y ) = GetCol(l, x, y)“ hinschreiben, weil man sonst keine info hat ob sich was geändert hat.

1 „Gefällt mir“

Hast recht, hab nicht dran gedacht, das auch nur eine Koordinate unterschiedlich bereits reicht…

Bin froh, das wenigstens mal ne ordentliche Lösung gefunden wurde :smiley:


so, ich habs mir nochmal durch den Kopf gehen lassen und mir ist dabei auch ein Denkfehler aufgefallen. Ich habe irgendiwie die Zustände von zwei verschieden Feldern gedanklich betrachtet, aber es geht ja immer nur um eins.

Daneben behaupte ich einfach mal, dass die Lösung einfacher sein muss, als hier bisher diskutiert wurde. Grundlage dafür ist ganz banal der verfügbare Schreibplatz.

Nehmen wir ein Feld(3,4)
und gehen wir davon aus, dass getX==3 und getY==4

Dann entspricht:
=> getCol(Step(l), x, y ) : dem Zustand des Feld(3, 4) nach dem step.
=> getCol( l , x , y ) : dem Zustand des selben Feldes vor dem step.

wir wissen, dass ein bolean Feld nie True und False sein kann :D.
Also wenn der Folgezustand vom Feld(3,4) true ist, dann muss er davor false gewesen sein.

Daher nehme ich an, dass gilt:

=> getCol(Step(l), x, y) = true AND !getCol(l, x, y) falls getX==x && getY==y

=> getCol(Step(l), x, y) = false sonst

jetzt wo ich den Sonst-Fall nochmal aufgeschrieben habe, muss ich dem Vorposter zustimmen, false geht hier nicht mangels infos.
Jedoch unter der vorherigen annahme, ist der Folgezustand in jedem Falle anders als der aktuelle Zustand des Feldes: (gilt Nur wenn die Ant auch auf dem Feld x,y war, was im sonst Fall nicht gegeben ist bzw. nicht mit Sicherheit angenommen werden kann)

=> getCol(Step(l), x, y) = getCol(l, x, y) sonst .

Teilaufgabe d)
Zu dem coding Teil, habt ihr das auch so verstanden, dass man nicht die ops getCol und getDir verwendet in der step implementierung?

Wie ist das mit den x, y werten, kann man die einfach als Ordinaten interpretieren oder muss ich die im Kontext fom raster[x][y] betrachten?
Je nachdem sieht halt das Ergebnis anders aus.

So hätt ich das in der Klausur gemacht:

class LangtonAntJava {
	boolean[][] raster = new boolean[4711][4242];
	int x = 666, y = 666, d = 0; // Position und Richtung

	public void step() {
		boolean col=raster[x][y];
		d=col?(d+1)%4:(d+3)%4;
		raster[x][y]=!col;
		
		switch(d){
		case 0:y++;break;
		case 1:x--;break;
		case 2:y--;break;
		case 3:x++;break;
		}
		
	}
}

Wenn ich das selbe so ausgeben möchte, so dass das Klausurbeispiel wiedergegeben wird, muss ich den switch-case seltsam umformen. Oder seht ihr ein Schnitzer?
>>testcode<<

public void step() {
		if(x < 0 || x >= raster.length || y < 0 || y >= raster.length )
			return;
 
		boolean col=raster[x][y];
		d=col?(d+1)%4:(d+3)%4;
		raster[x][y]=!col;
 
		switch(d){
		case 0:x--;break;
		case 1:y--;break;
		case 2:x++;break;
		case 3:y++;break;
		}
 
	}

In der Angabe steht: „d(0/1/2/3) =(N/W/S/O)“
Also ein doppeltes Array ist mit 0,0 immer von oben links zu betrachten.
------------->X
| [0,0][1,0]
| [0,1][1,1]
| [0,2][1,2]
v[color=crimson]
Y[/color]

daraus folgt

  switch(d){
        case 0:y--;break;//blickrichtung N -> y--
        case 1:x--;break;//W
        case 2:y++;break;//S
        case 3:x++;break;//O
        }

somit hat sich die „seltsame“ Umformung geklärt, beim Rest sehe ich keine Fehler, wobei ich zuerst die Methoden verwenden wollte, aber dann gemerkt habe, dass das keinen Sinn macht.

Zur 5 a) nochmal:
Ich glaube ich habe einen False-Fall vergessen, das ist wegen der blöden vorgegeben Schreibweise gewesen.
Ich würde es so darstellen:

                             ( True                 //if((x==l.getX()&& y==l.getY() && !getCol(l,x,y)
                             |
                             | False                //if((x==l.getX()&& y==l.getY() && getCol(l,x,y)

GetCol(Step(l), x, y ) =<
| getCol(l, x, y) //else
(

Seht jmd da einen Fehler?

b)

getDir(Step(l)) = (d+3)%4 falls !getCol(l, l.getX(), l.getY())
sonst = (d+1)%4

c)

                                                                Farbe: weiß                  UND    Richtung: N  ODER   Farbe: schwarz       UND  Richtung: S
                             ( getX()+1           //falls !getCol(l, l.getX(), l.getY()) ^ getDir(l) == 0 v getCol(l, l.getX(), l.getY()) ^ getDir(l) == 2
                             |                                  Farbe: schwarz             UND    Richtung: N  ODER   Farbe: weiß           UND  Richtung: S
                             | getX()- 1           //falls  getCol(l, l.getX(), l.getY()) ^ getDir(l) == 0 v !getCol(l, l.getX(), l.getY()) ^ getDir(l) == 2

getX(Step(l)) = <
| getCol(l, x, y) //sonst
(

Bei der bin ich mir jetzt gar nicht so sicher, wüsste aber nicht was man da sonst machen soll.