Algorithmic properties of nondeterministic programs are studied and axiomatized completely. Nondeterministic programs require two kinds of algorithmic formulas describing their behaviour: ΔKa – all computations of the program K are finite and all results satisfy a and ∇Ka – there exists a finite computation such that its result satisfies the formula a.