Tato práce definuje určitý typ vlastností počítačového programu. Dále popisuje způsob, jakým lze rozhodnout, zda daná část programu má, nebo nemá dané vlastnosti tohoto typu. Rozhodování probíhá bez potřeby program spustit a využívá teorii formálních jazyků. Součástí práce je prakticky použitelná knihovna, ve které jsou popsané postupy implementovány.This thesis defines a certain type of a computer program properties. It also describes how to decide whether or not given part of a program has given properties of this type. Deciding process does not need the program to be launched and it utilizes formal language theory. Part of the work is a practically usable library in which described methods are implemented.