Статья 300

К началу 70-х годов встали вопросы точного описания не только синтаксиса, но и семантики языков программирования.

В середине 60-х годов практически одновременно появился ряд пионерских работ в области описания условий, которым удовлетворяет программа. В.М. Глушков в 1965 г.

предложил алгоритмические алгебры впоследствии послужившие прообразом динамических логик, Ф.

Энгелер в 1967 г. - использование языков с бесконечно длинными формулами, чтобы выразить бесконечное множество возможностей, возникающих при разных исполнениях программы. Но наиболее популярны стали языки алгоритмических логик, которые включают высказывания вида, читающиеся следующим образом если до исполнения оператора было выполнено, то после него будет. Здесь называется предусловием, постусловием, либо обещанием.