Theorembeweisen in hierarchischen bedingten Spezifikationen |
| |
| Authors: | J Avenhaus und K Madlener |
| |
| Institution: | (1) Fachbereich Informatik, Universit?t Kaiserslautern, Erwin-Schr?dinger-Strasse, D-67663 Kaiserslautern , DE |
| |
| Abstract: | Zusammenfassung. In der Arbeit werden klausale Spezifikationen zur Beschreibung von Programmen auf der Ebene des funktionalen Entwurfs betrachtet.
Die Axiome solch einer Spezifikation bestehen aus positiv/negativ bedingten Gleichungen, die neue Operatoren über einer fest eingebauten Algebra definieren. Wir definieren als Semantik von eine Algebra , die initial in der Klasse aller Modelle ist. Es wird ein Inferenzsystem angegeben, mit dem man die Gültigkeit von positiv/negativ
bedingten Gleichungen in beweisen kann. Dieses Inferenzsystem erlaubt es auch, die Gültigkeit von Behauptungen zu widerlegen.
Eingegangen am 19. Juli 1994 / Angenommen am 7. November 1995 |
| |
| Keywords: | Schlüsselw?rter: Klausale Spezifikation partiell definierte Operatoren hierarchische Termersetzungssysteme induktives Beweisen |
| 本文献已被 SpringerLink 等数据库收录！ |
