Proving Concurrent Constraint Programs Correct

摘要

We develop a compositional proof-system for the partial correctness of concurrentconstraint programs. Soundness and (relative) completeness of the system are proved with respect to a denotational semantics based on the notion of strongest postcondition. The strongest post-condition semantics provides a justification of the declarative nature of concurrent constraint programs, since it allows to view programs as theories in the specification logic.