Формальная верификация: различия между версиями
| [отпатрулированная версия] | [непроверенная версия] |
Содержимое удалено Содержимое добавлено
Нет описания правки |
→Теоретические основы: дополнение |
||
Строка 16:
* формальная семантика языков программирования, например {{iw|операционная семантика||en|operational semantics}}, {{iw|денотационная семантика||en|denotational semantics}}, {{iw|аксиоматическая семантика||en|axiomatic semantics}} ([[логика Хоара]]), [[математическая семантика программ]]
* [[теория типов|теории]] и [[система типов|системы]] типов — в первую очередь, системы с [[зависимый тип|зависимыми типами]] (см. [[лямбда-куб]])
* [[логика разделения]] (расширение логики Хоара)
* [[конечный автомат]]
| |||