While-DS-interpreter

An interpreter for Denotational Semantics of While language

Abstract

The interpreter I takes in input a While program S and a state s, and applies the Denotational Semantics in order to return the final state I(S,s)=S_ds[S]s. S_ds[S]s=undef if and only if I(S,s) does not terminate. The interpreter relies on Kleene-Knaster-Tarski fixpoint iteration sequence for evaluating the while statements.

Architecture

Example

The following code implements in While language a function that stores on variable y the factorial of x and assigns 1 to x if x is a number greater or equal to 1 and does not terminate otherwise.

y := 1;
while !x=1 do(
  y := y*x;
  x := x-1
)

Let now define a state s = <x=4,y=10,z=3>. The interpreter with the statements above and the state s returns as final state <x=1,y=24,z=3> as expected.

Dependencies

• lark: library for parsing (https://github.com/erezsh/lark)