Niech x1, ... ,xn będą zmiennymi, n>0, 1≤i≤n. Każda formuła o podanym poniżej schemacie jest twierdzeniem running systemu Kreczmara.
co się czyta: jeżeli na pewien obiekt o wskazuje n zmiennych to po wykonaniu instrukcji kill(xi) wspólną wartością tych zmiennych jest none (oznacza to, że sam obiekt o jest od tej pory niedostępny i może być przez tę samą instrukcję kill bez szkody usunięty). W konsekwencji: nie ma potrzeby powtarzania operacji kill(x1),kill(x2), ... nie występuje zjawisko wiszących referencji, każda próba odniesienia się do atrybutu obiektu, który wcześniej został usunięty zostanie wykryta i spowoduje zgłoszenie wyjątku „reference to none”. Należy podkreślić, że koszt operacji kill jest stały, niezależny od liczby n wskaźników na usuwany obiekt. Taki system zarządzania pamięcią obiektów zastosowano tylko raz, w implementacji języka Loglan'82.
System zarządzania obiektami jest pomyślany całościowo, dostarcza operacji:
wspomagających powstanie obiektu – new, sprawdzających legalność operacji dostępu do atrybutów obiektu, usuwania obiektu na żądanie, defragmentacji i odśmiecania pamięci obiektowej.
Porównaj sposoby pozbywania się niepotrzebnych obiektów