bGSL: An Imperative Language for Specification and Refinement of Backtracking Programs

Abstract

We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference — the latter being a variant of Nelson’s biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non-monotonic program combinators.