Invarianten werden von Methodenaufruf und nach Methodenende gecheckt. Man kann damit viele requires und ensures Schreibarbeit sparen.
Falls ein Objekt obj verwendet wird, dann ist immer implizit requires obj ≠ null angewendet.
Falls man ein null zulassen will, muss man das explizit schreiben mit @nullable
C ist ein typ
asssignable /nothing - you can create new objects but cant manipulate existing
asssignable /stricktly_nothing - you cant create new objects and cant manipulate existing