A Refinement Calculus for Logic Programs

Details A Refinement Calculus for Logic Programs A Refinement Calculus for Logic Programs

2002-02-04

arxiv.org/abs/cs/0202002v1

Computer Science

Software Engineering

36 pages, 3 figures. To be published in Theory and Practice of Logic Programming (TPLP)

Scientific paper

Existing refinement calculi provide frameworks for the stepwise development of imperative programs from specifications. This paper presents a refinement calculus for deriving logic programs. The calculus contains a wide-spectrum logic programming language, including executable constructs such as sequential conjunction, disjunction, and existential quantification, as well as specification constructs such as general predicates, assumptions and universal quantification. A declarative semantics is defined for this wide-spectrum language based on executions. Executions are partial functions from states to states, where a state is represented as a set of bindings. The semantics is used to define the meaning of programs and specifications, including parameters and recursion. To complete the calculus, a notion of correctness-preserving refinement over programs in the wide-spectrum language is defined and refinement laws for developing programs are introduced. The refinement calculus is illustrated using example derivations and prototype tool support is discussed.

Affiliated with

Also associated with

No associations

Rating

A Refinement Calculus for Logic Programs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Refinement Calculus for Logic Programs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Refinement Calculus for Logic Programs will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-345725