Context induction: A proof principle for behavioural abstractions and algebraic implementations |
| |
Authors: | Rolf Hennicker |
| |
Affiliation: | (1) Fakultät für Mathematik und Informatik, Universität Passau, Postfach 2540, D-8390 Passau, Germany |
| |
Abstract: | An induction principle, called context induction, is presented which is appropriate for the verification of behavioural properties of abstract data types. The usefulness of the proof principle is documented by several applications: the verification of behavioural theorems over a behavioural specification, the verification of behavioural implementations and the verification of forget-restrict-identify implementations.In particular, it is shown that behavioural implementations and forget-restrict-identify implementations (under certain assumptions) can be characterised by the same condition on contexts, i.e. (under the given assumptions) both concepts are equivalent. This leads to the suggestion to use context induction as a uniform proof method for correctness proofs of algebraic implementations. |
| |
Keywords: | Context induction Behavioural specification Behavioural theorem Behavioural implementation FRI implementation |
本文献已被 SpringerLink 等数据库收录! |
|