P2 Skript 4.21

Kann mir jemand erklären wie ich folgendes verstehen bzw. interpretieren muss:

TYPES[G]

- STACK[]


FUNCTIONS

- push: STACK[G] –> G –>STACK[G]
- pop: STACK[G] -|-> STACK[G]
.
.

Ich weiß das push die Einfügeoperation für den Stack ist und pop die Ausfügeoperation ist, aber ich weiß nicht wie ich diese Notation zu verstehen habe.

AXIOMS

For any x:G, s:STACK[G]

- A1 top(push(s,x)) = x

Wie die Axiome definiert sind checke ich auch nicht.

AXIOMS

For any x:G, s:STACK[G]

- A1 top(push(s,x)) = x

Wie die Axiome definiert sind checke ich auch nicht.

Da steht eigentlich nur folgendes:
Wenn Du das Element x auf den Stack s drauftust (push), dann ist es auch wirklich oben drauf (top = s).

Ah…..das habe ich jetzt verstanden, und wie sieht es mit den Funktionen aus? Wie sind die zu verstehen?

FUNCTIONS

- push: STACK[G] –> G –>STACK[G]
- pop: STACK[G] -|-> STACK[G]
.
.
.

vielleicht
operationsname:erster Parameter (oder objekt an dem gerufen wird) -> 2. Parameter (-|-> für kein weiterer Parameter) -> Rückgabewert?

da wären etwas mehr Beispiele nützlich