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

Аксиоматска семантика је приступ заснован на математичкој логици за доказивање исправности рачунарских програма. Уско је повезан са Хоаре логиком. Аксиоматска семантика дефинише значење команде у програму описујући његов утицај на тврдње о стању програма. Наводe се логични изрази — предикати са варијаблама, гдје варијабле дефинишу стање програма.