Abstract
We formally prove in Isabelle/HOL two properties of an algorithm for laying out trees visually. The first property states that removing layout annotations recovers the original tree. The second property states that nodes are placed at least a unit of distance apart. We have yet to formalize three additional properties: That parents are centered above their children, that drawings are symmetrical with respect to reflection and that identical subtrees are rendered identically.
| Original language | English |
|---|---|
| Publication date | 2018 |
| Number of pages | 7 |
| Publication status | Published - 2018 |
| Event | Isabelle Workshop 2018 - Oxford, United Kingdom Duration: 13 Jul 2018 → 13 Jul 2018 http://sketis.net/isabelle/isabelle-workshop-2018 |
Workshop
| Workshop | Isabelle Workshop 2018 |
|---|---|
| Country/Territory | United Kingdom |
| City | Oxford |
| Period | 13/07/2018 → 13/07/2018 |
| Internet address |