stack of integers
-----------------
sorts Stack, Int, Bool
operations
	empty : -> Stack // constructor
	push : Stack Nat -> Stack // constructor
	pop : Stack -> Stack
	top : Stack -> Nat
	is-empty : Stack -> Bool
	error : -> Stack // constructor
variables
	var X : Nat
	var S : Stack
equations
	top(push(S,X)) = X
	top(empty) = error
	pop(push(S,X)) = S
	pop(empty) = error


sorted List
-----------
sorts: "List" (data structure) and "Int" (elements)

operations: constructor "empty_list()", "add(L, o)", "add(L, i, o)", "get(L, i)", "remove(L, i)", "size(L)", "contains(L, o)"

get(add(empty_list(), n), 0) = n
get(add(add(empty_list(), n), m), 0) = if (n < m) then n else m // without recursion but this approach requires chains of multiple calls to "add"
get(add(L, n), 0) = if (n < get(L, 0)) then n else get(L, 0) // recursion: we do not have to write chain (string) of multiple nested calls to "add"


ATM
---
state: number of available banknotes for each value (100, 200, 500, 1000, 2000)

operations:
	- card validation
	- checking account balance
	- cash withdrawal
	- cash deposit
	- retrieving account information from the central database of a respective bank
	- reading user PIN from keyboard

some declarations
	getAccount(card)
	validateCard(card, pin)
	withdrawMoney(ATM, account, amount)
	withdraw(ATM, card, pin, amount) = if validateCard(card, pin) then withdrawMoney(ATM, getAccount(card), amount) else exception("invalid")

modeling the state
	tuple (count100, count200, count500)
	to get 1800 CZK, the amount will be (0, 4, 2)