# 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 `ci` is fully evaluated Variable `xi,M → ci,M` where `M=c0,c1,c2,...` Composite `     e1,M → e'1,M'` `-----------------------` `e1 op e2,M → e'1 op e2,M'` `     e2,M → e'2,M'` `------------------------` `n1 op e2,M → n1 op e'2,M'` `n1 op n2,M → n3,M`, where `n3 = n1 op n2`

### Programs

 Null No rules as `null` is fully evaluated Assignment `    e,M → e',M' ` `-------------------` `xi:=e,M → xi:=e',M' ` `xi:=n,M → null,M{n/i} ` Sequence `    p1,M → p'1,M'` `----------------------` `(p1;p2),M → (p'1;p2),M'` `(null;p),M → p,M` Conditional `             b,M → b',M'` `-------------------------------------------------` `if b then p1 else p2,M → if b' then p1 else p2,M'` `if true then p1 else p2,M → p1,M` `if false then p1 else p2,M → p2,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.