공리적 의미론

공리적 의미론(axiomatic semantics)은 수리논리학을 기반으로 컴퓨터 프로그램의 정확성을 증명하는 접근 방식이다.^[1] 이는 호어 논리와 밀접하게 관련되어 있다.

공리적 의미론은 프로그램 상태에 대한 단언에 미치는 영향을 기술함으로써 프로그램 내 명령의 의미를 정의한다. 단언은 논리적 진술, 즉 변수가 있는 술어이며, 변수는 프로그램의 상태를 정의한다.

같이 보기

• 대수적 의미론 (컴퓨터 과학) — 대수적 관점
• 표시적 의미론 — 프로그램을 다른 언어로 변환하는 방식
• 동작적 의미론 — 계산의 상태 관점
• 프로그래밍 언어의 형식 의미론 — 개요
• 술어 변환기 의미론 — 프로그램 조각의 의미를 사후조건을 설정하는 데 필요한 선행조건으로 변환하는 함수로 설명한다.
• 어설션 (컴퓨팅)