Declarative Specification and Verification of Service Choreographies