Correctness and efficiency are important properties of programs. However, to support maintenance and debugging, the programs should also be understandable. Program explanations also play a vital role in educational settings, enhancing the understanding of programs among students.
Proof trees provide a sound basis for generating dynamic explanations of programs. But...