ABSTRACT
A logical constraint P can be interpreted both as a specification of system behaviour, and as a description of how P will be established in the system implementation.
These mean that a declarative high-level specification can be used for multiple purposes: (i) to express system functionality in a concise form, independent of code; (ii) to support verification at the specification level; (iii) as input for design and code synthesis to produce implementations in multiple target languages, which satisfy the specification by construction.
