Fact. Every while program can be simulated by a while program with at most one while loop.
Harel's proof using structural induction
Kozen's proof using KAT
Kleene Algebra with Tests (KAT)
Kozen's lecture notes on KAT
Kozen's result about the complexity & decidability of KAT
No comments:
Post a Comment