Behavioural Speciflcations 1
Rolf Hennicker, Martin Wirsing · 1995
In these lectures an observational approach to the semantics of algebraic specification is presented. Observability is defined in a logical way: an algebra is a behavioural model of a specification SP if it satisfies the axioms w.r.t. an observational interpretation of the equality relation. The advantages of this notion are proof-theoretic ones: the proof system for observational first-order formulae needs just one additional (in finitary) proof schema, the so-called context-induction. The completeness of this proof system for behavioural properties of a specification is shown. Examples for context-induction proofs are given and it is shown how by the theorem of Bidoit & Hennicker context-inductive properties can be proven without explicit use of context-induction. An ASL-like kernel language for modular behavioural specification is introduced and the correctness of refinements of specifications is studied. Sound and complete proof systems for properties of structured specifications and the validity of behavioural refinements are given. Moreover, behavioural refinement is transitive; the refinement of a subspecification SPO induces a correct refinement of the full specification SP if SP is behaviourally complete w.r.t. SPO.