A formalism for declarative specification and programming is introduced that forms a logical and methodological framework for program and system specification and construction. It combines axiomatic techniques based on logical concepts for specifying properties and the possibility to introduce names for objects. In particular it comprises within one formalism, the possibilities of formulating specifications and defining algorithms. The logical formalism is based more or less on typed predicate logic. The development rules are particular proof rules together with the inference rules of predicate logic. As a special aspect, the authors consider logical formulas which explicitly specify typed identifiers as elements of signatures.
展开▼
