KIT | KIT-Bibliothek | Impressum | Datenschutz

Proof obligations for monomorphicity

Schoenegge, Arno

Abstract:

In certain applications of formal methods to development of correct
software one wants the requirement specification to be monomorphic,
i.e. that every two term-generated models of it are isomorphic.
Consequently, the question arises how to guarantee monomorphicity
(which is not decidable in general). In this paper we show that the
task of proving monomorphicity of a specification can be reduced to a
task of proving certain properties of procedures (with indeterministic
constructs). So this task can be directly dealt with in the KIV
system (Karlsruhe Interactive Verifier) which was originally designed
for software verification. We prove correctness and completeness of
our method.


Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1995
Sprache Englisch
Identifikator urn:nbn:de:swb:90-AAA64953
KITopen-ID: 6495
Erscheinungsvermerk Karlsruhe 1995. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1995,34.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page