WHILE Interpreter

What is WHILE?

WHILE is a simple imperative programming language. It is used to learn the basic concepts of parsing, understanding, compiling verifying and executing programs.

Compared to other programming languages, WHILE is very constrained. This allows a simple machine like human brain to understand and analyze the programs. It consists of:
  1. Variables (x)
  2. Assignment (x := 1)
  3. Arithmetic expressions (x := 1 + 2)
  4. Boolean expressions (x > 0)
  5. While loops (while x > 0 do x := x - 1 end)
  6. Conditional statements (if x > 0 then x := x - 1 else x := x + 1 end)
So as a it's turing complete, it should be more than enough for any real programmer.

(For full mathematical definition of the language, see here)

Try it out!

Example programs:
Disclaimer! Your program contains the while loop. We can't determine if your program will terminate, so if your browser freezes, you were warned! If you know how to check if an arbitrary program terminates, please let us know!

Free Variables

x:=x :=

Results

Final State ( σ(Var)\sigma(Var) )

x y
1 6

Execution trace ( Σ\Sigma )

6 Steps

Derivation

Derivation Tree

(number)
⟨1,σ1⟩→1⟨1,σ1⟩→1=:z1 \begin{align} \Braket{ 1, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow 1 =: z_{1} \end{align}
(Cmd_assign)
⟨y:=1,σ1⟩→σ1[y↦1]=:σ2⟨y:=a0,σ1⟩→σ1[y↦z1]=:σ2 \begin{align} \Braket{ y:=1, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow \color{#fef3c7} \sigma_{1} \color{unset} [ y \mapsto 1 ] =: \color{#fef08a} \sigma_{2} \color{unset} \\ \Braket{ y := a_{0}, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow \color{#fef3c7} \sigma_{1} \color{unset} [ y \mapsto z_{1} ] =: \color{#fef08a} \sigma_{2} \color{unset} \end{align}
(var)
⟨x,σ2⟩→3⟨x,σ2⟩→σ(x)=:z2 \begin{align} \Braket{ x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 3 \\ \Braket{ x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \sigma(x) =: z_{2} \end{align}
(number)
⟨1,σ2⟩→1⟨1,σ2⟩→1=:z3 \begin{align} \Braket{ 1, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 1 =: z_{3} \end{align}
(PriBExp)
if ¬(z2=z3)\text{if } \neg (z_{2} = z_{3})
⟨x=1,σ2⟩→false⟨a1=a2,σ2⟩→b1 \begin{align} \Braket{ x = 1, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow false \\ \Braket{ a_{1} = a_{2}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow b_{1} \end{align}
(BExp_not)
⟨¬ (x=1),σ2⟩→true⟨¬ b1,σ2⟩→true=:b0 \begin{align} \Braket{ \neg\ ( x = 1 ), \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow true \\ \Braket{ \neg\ b_{1}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow true =: b_{0} \end{align}
(var)
⟨y,σ2⟩→1⟨y,σ2⟩→σ(y)=:z5 \begin{align} \Braket{ y, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 1 \\ \Braket{ y, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \sigma(y) =: z_{5} \end{align}
(var)
⟨x,σ2⟩→3⟨x,σ2⟩→σ(x)=:z6 \begin{align} \Braket{ x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 3 \\ \Braket{ x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \sigma(x) =: z_{6} \end{align}
(AExp_mul)
where z4:=z5∗z6\text{where } z_{4} := z_{5} * z_{6}
⟨y∗x,σ2⟩→3⟨a4∗a5,σ2⟩→z4 \begin{align} \Braket{ y*x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow 3 \\ \Braket{ a_{4} * a_{5}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow z_{4} \end{align}
(Cmd_assign)
⟨y:=y∗x,σ2⟩→σ2[y↦3]=:σ3⟨y:=a3,σ2⟩→σ2[y↦z4]=:σ3 \begin{align} \Braket{ y:=y*x, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#fef08a} \sigma_{2} \color{unset} [ y \mapsto 3 ] =: \color{#fde68a} \sigma_{3} \color{unset} \\ \Braket{ y := a_{3}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#fef08a} \sigma_{2} \color{unset} [ y \mapsto z_{4} ] =: \color{#fde68a} \sigma_{3} \color{unset} \end{align}
(var)
⟨x,σ3⟩→3⟨x,σ3⟩→σ(x)=:z8 \begin{align} \Braket{ x, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow 3 \\ \Braket{ x, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow \sigma(x) =: z_{8} \end{align}
(number)
⟨1,σ3⟩→1⟨1,σ3⟩→1=:z9 \begin{align} \Braket{ 1, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow 1 =: z_{9} \end{align}
(AExp_sub)
where z7:=z8−z9\text{where } z_{7} := z_{8} - z_{9}
⟨x−1,σ3⟩→2⟨a7−a8,σ3⟩→z7 \begin{align} \Braket{ x-1, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow 2 \\ \Braket{ a_{7} - a_{8}, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow z_{7} \end{align}
(Cmd_assign)
⟨x:=x−1,σ3⟩→σ3[x↦2]=:σ4⟨x:=a6,σ3⟩→σ3[x↦z7]=:σ4 \begin{align} \Braket{ x:=x-1, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow \color{#fde68a} \sigma_{3} \color{unset} [ x \mapsto 2 ] =: \color{#fde047} \sigma_{4} \color{unset} \\ \Braket{ x := a_{6}, \color{#fde68a} \sigma_{3} \color{unset} } &\rightarrow \color{#fde68a} \sigma_{3} \color{unset} [ x \mapsto z_{7} ] =: \color{#fde047} \sigma_{4} \color{unset} \end{align}
(Cmd_seq)
⟨y:=y∗x ; x:=x−1,σ2⟩→σ4⟨c3 ; c4,σ2⟩→σ4 \begin{align} \Braket{ \color{#bae6fd} y:=y * x \color{unset} \text{ ; } \color{#f5d0fe} x:=x - 1 \color{unset}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#fde047} \sigma_{4} \color{unset} \\ \Braket{ \color{#bae6fd} c_{3} \color{unset} \text{ ; } \color{#f5d0fe} c_{4} \color{unset}, \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#fde047} \sigma_{4} \color{unset} \end{align}
(var)
⟨x,σ4⟩→2⟨x,σ4⟩→σ(x)=:z11 \begin{align} \Braket{ x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 2 \\ \Braket{ x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \sigma(x) =: z_{11} \end{align}
(number)
⟨1,σ4⟩→1⟨1,σ4⟩→1=:z12 \begin{align} \Braket{ 1, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 1 =: z_{12} \end{align}
(PriBExp)
if ¬(z11=z12)\text{if } \neg (z_{11} = z_{12})
⟨x=1,σ4⟩→false⟨a9=a10,σ4⟩→b3 \begin{align} \Braket{ x = 1, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow false \\ \Braket{ a_{9} = a_{10}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow b_{3} \end{align}
(BExp_not)
⟨¬ (x=1),σ4⟩→true⟨¬ b3,σ4⟩→true=:b2 \begin{align} \Braket{ \neg\ ( x = 1 ), \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow true \\ \Braket{ \neg\ b_{3}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow true =: b_{2} \end{align}
(var)
⟨y,σ4⟩→3⟨y,σ4⟩→σ(y)=:z14 \begin{align} \Braket{ y, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 3 \\ \Braket{ y, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \sigma(y) =: z_{14} \end{align}
(var)
⟨x,σ4⟩→2⟨x,σ4⟩→σ(x)=:z15 \begin{align} \Braket{ x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 2 \\ \Braket{ x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \sigma(x) =: z_{15} \end{align}
(AExp_mul)
where z13:=z14∗z15\text{where } z_{13} := z_{14} * z_{15}
⟨y∗x,σ4⟩→6⟨a12∗a13,σ4⟩→z13 \begin{align} \Braket{ y*x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow 6 \\ \Braket{ a_{12} * a_{13}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow z_{13} \end{align}
(Cmd_assign)
⟨y:=y∗x,σ4⟩→σ4[y↦6]=:σ5⟨y:=a11,σ4⟩→σ4[y↦z13]=:σ5 \begin{align} \Braket{ y:=y*x, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#fde047} \sigma_{4} \color{unset} [ y \mapsto 6 ] =: \color{#fcd34d} \sigma_{5} \color{unset} \\ \Braket{ y := a_{11}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#fde047} \sigma_{4} \color{unset} [ y \mapsto z_{13} ] =: \color{#fcd34d} \sigma_{5} \color{unset} \end{align}
(var)
⟨x,σ5⟩→2⟨x,σ5⟩→σ(x)=:z17 \begin{align} \Braket{ x, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow 2 \\ \Braket{ x, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow \sigma(x) =: z_{17} \end{align}
(number)
⟨1,σ5⟩→1⟨1,σ5⟩→1=:z18 \begin{align} \Braket{ 1, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow 1 =: z_{18} \end{align}
(AExp_sub)
where z16:=z17−z18\text{where } z_{16} := z_{17} - z_{18}
⟨x−1,σ5⟩→1⟨a15−a16,σ5⟩→z16 \begin{align} \Braket{ x-1, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow 1 \\ \Braket{ a_{15} - a_{16}, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow z_{16} \end{align}
(Cmd_assign)
⟨x:=x−1,σ5⟩→σ5[x↦1]=:σ6⟨x:=a14,σ5⟩→σ5[x↦z16]=:σ6 \begin{align} \Braket{ x:=x-1, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow \color{#fcd34d} \sigma_{5} \color{unset} [ x \mapsto 1 ] =: \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ x := a_{14}, \color{#fcd34d} \sigma_{5} \color{unset} } &\rightarrow \color{#fcd34d} \sigma_{5} \color{unset} [ x \mapsto z_{16} ] =: \color{#facc15} \sigma_{6} \color{unset} \end{align}
(Cmd_seq)
⟨y:=y∗x ; x:=x−1,σ4⟩→σ6⟨c6 ; c7,σ4⟩→σ6 \begin{align} \Braket{ \color{#bae6fd} y:=y * x \color{unset} \text{ ; } \color{#f5d0fe} x:=x - 1 \color{unset}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ \color{#bae6fd} c_{6} \color{unset} \text{ ; } \color{#f5d0fe} c_{7} \color{unset}, \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \end{align}
(var)
⟨x,σ6⟩→1⟨x,σ6⟩→σ(x)=:z20 \begin{align} \Braket{ x, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow 1 \\ \Braket{ x, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow \sigma(x) =: z_{20} \end{align}
(number)
⟨1,σ6⟩→1⟨1,σ6⟩→1=:z21 \begin{align} \Braket{ 1, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow 1 \\ \Braket{ 1, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow 1 =: z_{21} \end{align}
(PriBExp)
if z20=z21\text{if } z_{20} = z_{21}
⟨x=1,σ6⟩→true⟨a17=a18,σ6⟩→b5 \begin{align} \Braket{ x = 1, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow true \\ \Braket{ a_{17} = a_{18}, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow b_{5} \end{align}
(BExp_not)
⟨¬ (x=1),σ6⟩→false⟨¬ b5,σ6⟩→false=:b4 \begin{align} \Braket{ \neg\ ( x = 1 ), \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow false \\ \Braket{ \neg\ b_{5}, \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow false =: b_{4} \end{align}
(while-false)
⟨while ¬(x=1) do y:=y∗x;x:=x−1 end,σ6⟩→σ6⟨while b4 do c8 end,σ6⟩→σ6 \begin{align} \Braket{ \text{while } \color{#a7f3d0} \neg ( x = 1 ) \color{unset} \text{ do } \color{#bae6fd} y:=y * x;x:=x - 1 \color{unset} \text{ end} , \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ \text{while } \color{#a7f3d0} b_{4} \color{unset} \text{ do } \color{#bae6fd} c_{8} \color{unset} \text{ end} , \color{#facc15} \sigma_{6} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \end{align}
(while-true)
⟨while ¬(x=1) do y:=y∗x;x:=x−1 end,σ4⟩→σ6⟨while b2 do c5 end,σ4⟩→σ6 \begin{align} \Braket{ \text{while } \color{#a7f3d0} \neg ( x = 1 ) \color{unset} \text{ do } \color{#bae6fd} y:=y * x;x:=x - 1 \color{unset} \text{ end} , \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ \text{while } \color{#a7f3d0} b_{2} \color{unset} \text{ do } \color{#bae6fd} c_{5} \color{unset} \text{ end} , \color{#fde047} \sigma_{4} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \end{align}
(while-true)
⟨while ¬(x=1) do y:=y∗x;x:=x−1 end,σ2⟩→σ6⟨while b0 do c2 end,σ2⟩→σ6 \begin{align} \Braket{ \text{while } \color{#a7f3d0} \neg ( x = 1 ) \color{unset} \text{ do } \color{#bae6fd} y:=y * x;x:=x - 1 \color{unset} \text{ end} , \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ \text{while } \color{#a7f3d0} b_{0} \color{unset} \text{ do } \color{#bae6fd} c_{2} \color{unset} \text{ end} , \color{#fef08a} \sigma_{2} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \end{align}
(Cmd_seq)
⟨y:=1 ; while ¬(x=1) do y:=y∗x;x:=x−1 end,σ1⟩→σ6⟨c0 ; c1,σ1⟩→σ6 \begin{align} \Braket{ \color{#bae6fd} y:=1 \color{unset} \text{ ; } \color{#f5d0fe} \text{while } \neg ( x = 1 ) \text{ do } y:=y * x;x:=x - 1 \text{ end} \color{unset}, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \\ \Braket{ \color{#bae6fd} c_{0} \color{unset} \text{ ; } \color{#f5d0fe} c_{1} \color{unset}, \color{#fef3c7} \sigma_{1} \color{unset} } &\rightarrow \color{#facc15} \sigma_{6} \color{unset} \end{align}

Machine Code

Disclaimer! This part partly appeared in the lecture. But it's (still) just authors' interpretation, motivated by implementation details and previous preconceptions.
Warning! The computation chains can get pretty long and the TeX renderer isn't a fan of that. So when choosing Math the browser might get slow.
Step Instruction PC Stack State
1 PUSH( 1 ) 1 [1] { x → 3 }
2 STO( y ) 2 [] { x → 3; y → 1 }
3 LOAD( x ) 3 [3] { x → 3; y → 1 }
4 PUSH( 1 ) 4 [3:1] { x → 3; y → 1 }
5 EQ 5 [false] { x → 3; y → 1 }
6 NOT 6 [true] { x → 3; y → 1 }
7 JMPF( 17 ) 7 [] { x → 3; y → 1 }
8 LOAD( y ) 8 [1] { x → 3; y → 1 }
9 LOAD( x ) 9 [1:3] { x → 3; y → 1 }
10 MULT 10 [3] { x → 3; y → 1 }
11 STO( y ) 11 [] { x → 3; y → 3 }
12 LOAD( x ) 12 [3] { x → 3; y → 3 }
13 PUSH( 1 ) 13 [3:1] { x → 3; y → 3 }
14 SUB 14 [2] { x → 3; y → 3 }
15 STO( x ) 15 [] { x → 2; y → 3 }
16 JMP( 3 ) 2 [] { x → 2; y → 3 }
17 LOAD( x ) 3 [2] { x → 2; y → 3 }
18 PUSH( 1 ) 4 [2:1] { x → 2; y → 3 }
19 EQ 5 [false] { x → 2; y → 3 }
20 NOT 6 [true] { x → 2; y → 3 }
21 JMPF( 17 ) 7 [] { x → 2; y → 3 }
22 LOAD( y ) 8 [3] { x → 2; y → 3 }
23 LOAD( x ) 9 [3:2] { x → 2; y → 3 }
24 MULT 10 [6] { x → 2; y → 3 }
25 STO( y ) 11 [] { x → 2; y → 6 }
26 LOAD( x ) 12 [2] { x → 2; y → 6 }
27 PUSH( 1 ) 13 [2:1] { x → 2; y → 6 }
28 SUB 14 [1] { x → 2; y → 6 }
29 STO( x ) 15 [] { x → 1; y → 6 }
30 JMP( 3 ) 2 [] { x → 1; y → 6 }
31 LOAD( x ) 3 [1] { x → 1; y → 6 }
32 PUSH( 1 ) 4 [1:1] { x → 1; y → 6 }
33 EQ 5 [true] { x → 1; y → 6 }
34 NOT 6 [false] { x → 1; y → 6 }
35 JMPF( 17 ) 16 [] { x → 1; y → 6 }