Аксиоматическая семантика

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

Аксиоматическая семантика определяет значение команды в программе, описывая ее влияние на утверждения о состоянии программы. Утверждения представляют собой логические утверждения - предикаты с переменными, где переменные определяют состояние программы.

• Алгебраическая семантика (информатика) - в терминах алгебр
• Денотационная семантика - путем перевода программы на другой язык
• Операционная семантика - в терминах состояния вычислений
• Формальная семантика языков программирования - обзор
• Семантика преобразователя предикатов - описывает значение фрагмента программы как функцию, преобразующую постусловие к предварительному условию, необходимому для его установки.
• Утверждение (вычисление)

.