Structured Transition Semantics

We can use a terminal transition system to describe the semantics of a programming language. Here we show how the semantics for the language IMP can be given without using a low-level interpreter such as the SMC machine. This is done by giving as a set of evaluation rules as an inductive definition of a transition system relation. The result is a structured transition semantics for the language IMP.

Structured Transition Semantics for IMP

We now define a set of rules for the transition relation →∈(Phrases×Memories)×(Phrases×Memories).

Expressions

Constant	No rules as `c_i` is fully evaluated
Variable	`x_i,M → c_i,M` where `M=c₀,c₁,c₂,...`
Composite	`e₁,M → e'₁,M'` `-----------------------` `e₁ op e₂,M → e'₁ op e₂,M'` `e₂,M → e'₂,M'` `------------------------` `n₁ op e₂,M → n₁ op e'₂,M'` `n₁ op n₂,M → n₃,M`, where `n₃ = n₁ op n₂`

Programs

Null	No rules as `null` is fully evaluated
Assignment	`e,M → e',M'` `-------------------` `x_i:=e,M → x_i:=e',M'` `x_i:=n,M → null,M{n/i}`
Sequence	`p₁,M → p'₁,M'` `----------------------` `(p₁;p₂),M → (p'₁;p₂),M'` `(null;p),M → p,M`
Conditional	`b,M → b',M'` `-------------------------------------------------` `if b then p₁ else p₂,M → if b' then p₁ else p₂,M'` `if true then p₁ else p₂,M → p₁,M` `if false then p₁ else p₂,M → p₂,M`
Iteration	`while b do p,M → if b then (p;while b do p) else null,M`

In the above, the notation M{n/i} means the i^th memory value is set to n.

The set of configurations, Γ=Phrases×Memories, and the transition relation, →, give us the transition system. When we define the set of terminal states as {(null,M)|M∈Memories}, we have a terminal transition system. Note that this terminal transition system is monogenic. Note also that the evaluation order of expressions has been determined - left subexpression, then right subexpression - and this is quite arbitrary.

Implementation

The following code was written and tested in Barry's Prolog as an example implementation of the structured transition semantics of the IMP language. This should work on almost any ISO compliant Prolog system.

	
%%%
%%% Configure the operators.
%%%
:- op(0, xfx, =>).
:- op(800, xfx, =>).

%%%
%%% sts_constant(+C)
%%%
%%% Succeeds if C is a constant.
%%%
sts_constant(C) :-
	number(C).

%%%
%%% sts_mem_get(+M, +A, -V)
%%%
%%% V is the value stored in memory M at address A.
%%%
sts_mem_get(M, A, V) :-
	(member(A-V, M)
    ;
	V = 0),
	!.

%%%
%%% sts_mem_put(+Min, +A, +V, Mout)
%%%
%%% Store the value V in memory Min at address A giving Mout.
%%%
sts_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 structured transition semantics.
%%%
(var(I), M) => (Value, M) :- % Variable
	sts_mem_get(M, var(I), Value).

(E1, M1) => (E2, M2) :- % Composite (1)
	compound(E1),
	E1 =.. [Op, Left1, Right],
	compound(Left1),
	member(Op, [+, -, *, /, =, <, >]),
	!,
	(Left1, M1) => (Left2, M2),
	E2 =.. [Op, Left2, Right].
(E1, M1) => (E2, M2) :- % Composite (2)	
	compound(E1),
	E1 =.. [Op, Left, Right1],
	sts_constant(Left),
	compound(Right1),
	member(Op, [+, -, *, /, =, <, >]),
	!,
	(Right1, M1) => (Right2, M2),
	E2 =.. [Op, Left, Right2].
(E1, M) => (E2, M) :- % Composite (3) Integer
	compound(E1),
	E1 =.. [Op, Left, Right],
	sts_constant(Left),
	sts_constant(Right),
	member(Op, [+, -, *, /]),
	!,
	E2 is E1.
(E1, M) => (E2, M) :- % Composite (3) Boolean
	compound(E1),
	E1 =.. [Op, Left, Right],
	sts_constant(Left),
	sts_constant(Right),
	member(Op, [=, <, >]),
	!,
	(call(E1) -> E2 = true ; E2 = false).

(assign(var(I), N), M1) => (null, M2) :- % Assignment (2)
	sts_constant(N),
	!,
	sts_mem_put(M1, var(I), N, M2).
(assign(var(I), E1), M1) => (assign(var(I), E2), M2) :- % Assignment (1)
	(E1, M1) => (E2, M2).

((null;P),M) => (P,M) :- % Sequence (2)
	!.
((P1;P2),M1) => ((P3;P2),M2) :- % Sequence (1)
	(P1,M1) => (P3,M2).

(if(true,P,_),M) => (P,M) :- % Conditional (2)
	!.
(if(false,_,P),M) => (P,M) :- % Conditional (3)
	!.
(if(B1,P1,P2),M1) => (if(B2,P1,P2),M2) :- % Conditional (1)
	(B1,M1) => (B2,M2).

(while(B,P), M) => (if(B,(P;while(B,P)),null),M). % Iteration

%%%
%%% run_sts(+S1, -S2)
%%%
%%% S1 =>* S2
%%%
run_sts(Input, Output) :-
	Input => Mid,
	!,
	run_sts(Mid, Output).
run_sts(Output, Output). % No transition possible.

%%%
%%% test_sts(+P, -M)
%%%
%%% M is the result (memory) of executing program P if it terminates correctly,
%%% i.e is tranformed into null.
%%%
%%% Example:
%%%
%%% | ?- test_sts(assign(var(1), 3+4), M).
%%% M = [var(1)-7] ? 
%%%
%%% % yes
%%%
%%% test_sts(if(2<3, assign(var(1), 1), assign(var(1), 0)), M).
%%% test_sts(while(var(1)<5, (assign(var(1), var(1)+1); assign(var(2), var(2)+2))), M).
%%%
test_sts(Program, Memory) :-
	run_sts((Program,[]), (null,Memory)).

References

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