We can use a terminal transition system to describe the semantics of a programming language. Here we show how an interpreter for the language IMP can be given without writing this interpreter in another language. This is done by designing the interpreter as an abstract machine which is defined as a terminal transition system.

The state of the machine consists of three components

- A value stack
`S`

∈Phrases^{*} - A memory
`M`

∈Constants^{∞} - A control stack
`C`

∈(Phrases∪Operations∪{`if`

,`assign`

,`while`

})^{*}

The value stack will contain the results of evaluation and phrases which have been deferred.

The memory `M=c`

contains the current values of the variables
_{0},c_{1},c_{2},...`x`

.
The memory has been made infinite to avoid placing a bound on the number of variables.
_{0},x_{1},x_{2},...

The control stack holds phrases whose execution has not begun.

The transition relation between configurations is `⇒`

.
It is defined by the rules below.
In these rules the concatenation operator (`:`

) is used to build stacks.
The empty stack is `ε`

and `X:ε`

=`X`

is a stack of one element.

Constant | `⟨S, M, c:C⟩⇒⟨c:S, M, C⟩` |

Variable | `⟨S, M, x` where `M=c` |

Composite | `⟨S, M, (e` |

Operator | `⟨n` where `n` is the evaluation of `n` |

Null | `⟨S, M, null:C⟩⇒⟨S, M, C⟩` |

Assignment | `⟨S, M, (X` |

Sequence | `⟨S, M, (p` |

Conditional | `⟨S, M, (if b then p` |

Iteration | `⟨S, M, (while b do p):C⟩⇒⟨b:p:S, M, b:while:C⟩` |

`assign`

, `if`

and `while`

Assign | `⟨n:i:s:S, M, assign:C⟩⇒⟨S, M{n/i}, C⟩` |

If | `⟨true:p` `⟨false:p` |

While | `⟨true:b:p:S, M, while:C⟩⇒⟨S, M, p:(while b do p):C⟩` `⟨false:b:p:S, M, while:C⟩⇒⟨S, M, C⟩` |

The notation `M{n/i}`

means the i^{th} memory value is set to `n`

.

We've defined a set of configurations and the transition relation `⇒`

but we've not defined the
set of terminal configurations.
We can define this set to be all the configurations of the form `⟨ε, M, ε⟩`

.
Provided the program `p`

terminates, it will always be the case that
`⟨ε, M, p⟩⇒`

.
^{*}⟨ε, M, ε⟩

The SMC transition system is monogenic.

We can define an evaluation function,
EVAL:Programs→(Memories→Memories),
which is a partial function over Memories:
EVAL(`p`

)(`M`

) = `M'`

if `⟨ε, M, p;⟩⇒`

,
otherwise the result is undefined.
The fact that the transition system is monogenic means that this is a proper function.
^{*}⟨ε, M', ε⟩

The following is an implementation of the SMC machine written in Barry's Prolog. It should run on any ISO compliant Prolog system.

```
```%%%
%%% Configure the operators.
%%%
:- op(0, xfx, =>).
:- op(800, xfx, =>).
%%%
%%% smc_constant(+C)
%%%
%%% Succeeds if C is an SMC constant
%%%
smc_constant(C) :-
number(C).
%%%
%%% smc_mem_get(+M, +A, -V)
%%%
%%% V is the value stored in memory M at address A.
%%%
smc_mem_get(M, A, V) :-
(member(A-V, M)
;
V = 0),
!.
%%%
%%% smc_mem_put(+Min, +A, +V, Mout)
%%%
%%% Store the value V in memory Min at address A giving Mout.
%%%
smc_mem_put(Min, A, V, Mout) :-
(del(A-_, Min, Mmid)
;
Mmid = Min),
!,
Mout = [A-V|Mmid].
%%%
%%% +State1 => -State2
%%%
%%% '=>'/2 is the transition relation for the SMC machine.
%%%
(S, M, [Constant|C]) => ([Constant|S], M, C) :- % Constant
smc_constant(Constant).
(S, M, [var(I)|C]) => ([Value|S], M, C) :- % Variable
smc_mem_get(M, var(I), Value).
(S, M, [E|C]) => (S, M, [E1, E2, Op|C]) :- % Composite
compound(E),
E =.. [Op, E1, E2],
member(Op, [+, -, *, /, =, <, >]).
([N2, N1|S], M, [Op|C]) => (S, M, [Value|C]) :- % Operator
number(N1),
number(N2),
member(Op, [+, -, *, /]),
Expression =.. [Op, N1, N2],
Value is Expression.
([N2, N1|S], M, [Op|C]) => ([Value|S], M, C) :- % Operator
number(N1),
number(N2),
member(Op, [=, <, >]),
Call =.. [Op, N1, N2],
(call(Call) -> Value = true ; Value = false).
(S, M, [null|C]) => (S, M, C). % Null
(S, M, [assign(var(I), E)|C]) => ([var(I)|S], M, [E, assign|C]). % Assignment
(S, M, [(P1;P2)|C]) => (S, M, [P1,P2|C]). % Sequence
(S, M, [if(B,P1,P2)|C]) => ([P1,P2|S], M, [B, if|C]). % Conditional
(S, M, [while(B,P1)|C]) => ([B, P1|S], M, [B, while|C]). % Iteration
([N,var(I)|S], M1, [assign|C]) => (S, M2, C) :- % Assign
smc_constant(N),
smc_mem_put(M1, var(I), N, M2).
([true, P1, _|S], M, [if|C]) => (S, M, [P1|C]). % If
([false, _, P2|S], M, [if|C]) => (S, M, [P2|C]). % If
([true, B, P1|S], M, [while|C]) => (S, M, [P1,while(B, P1)|C]). % While
([false, _, _|S], M, [while|C]) => (S, M, C). % While
%%%
%%% run_smc(+S1, -S2)
%%%
%%% S1 =>* S2
%%%
run_smc(Input, Output) :-
Input => Mid,
!,
run_smc(Mid, Output).
run_smc(Output, Output).
%%%
%%% test_smc(+P, -M)
%%%
%%% M is the result (memory) of executing program P.
%%%
%%% Example:
%%%
%%% | ?- test_smc(assign(var(1), 3+4), M).
%%% M = [var(1)-7] ?
%%%
%%% % yes
%%%
%%% test_smc(if(2<3, assign(var(1), 1), assign(var(1), 0)), M).
%%% test_smc(while(var(1)<5, (assign(var(1), var(1)+1); assign(var(2), var(2)+2))), M).
test_smc(Program, Memory) :-
run_smc(([], [], [Program]), ([], Memory, [])).

R. Burstall. *Language Semantics and Implementation. Course Notes.* 1994.

Copyright © 2014 Barry Watson. All rights reserved.