От неформальных высказываний перейдем к простой математической нотации, принятой в теории формальной проверки правильности программ и имеющей ценность при доказательстве корректности программных элементов.