Ordered and continuous models of higher-order specifications

We investigate the existence of continuous and fixpoint models of higher-order specifications. Particular attention is paid to the question of extensionality. We use ordered specifications, a particular case of Horn specifications. The main tool for obtaining continuous models is the ideal completion. Unfortunately, it may destroy extensionality. This problem is inherent: we show that there is no completion method which is guaranteed to preserve extensionality. To restore it, generally a quotient has to be taken. It is shown that under certain conditions this preserves the existence of least fixpoints. Examples of the specification method include the essential concepts of Backus's FP and Hoare's CSP.