Declarative constraint modelling and specification-level reasoning