Аксиоматическая семантика
| Семантика | ||||||||
|---|---|---|---|---|---|---|---|---|
| ||||||||
| Семантика языки программирования | ||||||||
| ||||||||
 | Эта статья нуждается в дополнительных цитатах для проверки . ( декабрь 2021 г. ) |
Аксиоматическая семантика — это подход, основанный на математической логике для доказательства правильности компьютерных программ . [1] Она тесно связана с логикой Хоара .
Аксиоматическая семантика определяет значение команды в программе, описывая ее влияние на утверждения о состоянии программы. Утверждения представляют собой логические операторы — предикаты с переменными, где переменные определяют состояние программы.
См. также [ править ]
- Алгебраическая семантика (информатика) - с точки зрения алгебр.
- Денотационная семантика — путем перевода программы на другой язык.
- Операционная семантика - с точки зрения состояния вычислений
- Формальная семантика языков программирования — обзор
- Семантика преобразователя предикатов — описывает значение фрагмента программы как функции, преобразующей постусловие в предусловие, необходимое для его установления.
- Утверждение (вычисление)
Ссылки [ править ]
- ^ Винскель, Глинн (5 февраля 1993 г.). Формальная семантика языков программирования: введение . МТИ Пресс. ISBN 978-0-262-73103-4 .
 | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |