Diagram Chase in Relational System Development |
| |
| Authors: | Michael Ebert Georg Struth |
| |
| Affiliation: | Department of Computer Science, University of the Federal Armed Forces Munich, Germany |
| |
| Abstract: | We propose diagrammatic techniques for visualizing relational reasoning in formal methods like B or Z; in particular for induction and coinduction. These are similar to those for functional diagrams in category theory and inspired by rewriting theory. Diagrams are endowed with a simple algebraic semantics that imposes a convenient balance between expressive and algorithmic power. This makes the approach particularly suitable for mechanization and automation. Its usefulness for visual reasoning is illustrated by various examples. |
| |
| Keywords: | diagrams semi-commutation formal semantics relational system development B Z induction coinduction iterator algebras |
| 本文献已被 ScienceDirect 等数据库收录！ |
