공통:

• Expression의 meaning을 $Expr → State → Value$ 타입의 total 함수로 표현한다.
• Program의 meaning은 $State \hookrightarrow State$ 타입의 partial 함수이다.

상이:

• Statement $S$를 나타내는 방식

Operational

program이 어떻게 실행되는지 집중하고, 실행 결과는 기술하지 않는다.

Statement $S$에 대해서만 다룸

공통:

• transition system $(\mathbb S, \rarr)$ 구성, configuration $\mathbb S$
• Statement의 meaning을 $Stmt \rarr State \hookrightarrow State$ 타입의 partial 함수로 표현한다.

상이:

• transition relation $(\rarr)$

Big-step

transition relation을 inference rule(proof rule)로 정의한다.

transition relation의 두 번째 configuration에 terminal state만 등장한다.

program 실행은 derivation tree를 생성하는 과정이다.

Statement $S$의 meaning을 (Statement $S$, initial state $s$, final state $s^\prime$)의 tuple로 표현한다.

Execution Type:

• terminates: derivation tree가 유한