An interpreter for Denotational Semantics of While language
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.
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.
- lark: library for parsing (https://github.com/erezsh/lark)