This paper focuses on the integration of reachability and observability
concepts within an algebraic, institution-based framework. We develop the
essential notions that are needed to construct an institution which takes
into account both the generation- and observation-oriented aspects of software
systems. Thereby the underlying paradigm is that the semantics of a
specification should be as loose as possible to capture all its correct
realizations. We also consider the so-called ``idealized models'' of a
specification which are useful to study the behavioral properties a user
can observe when he/she is experimenting with the system. Finally, we
present sound and complete proof systems that allow us to derive behavioral
properties from the axioms of a given specification.