Refining Real Valued Specifications to Floating Point Programs: A Case Study
Anthony Bloesch
Software Verification Research Centre,
Department of Computer Science,
University of Queensland, 4072, Australia.
anthonyb@cs.uq.edu.au
Ed Kazmierczak
Software Verification Research Centre,
Department of Computer Science,
University of Queensland, 4072, Australia.
Abstract
Specifications involving real numbers are likely to be unimplementable but
specifications involving floating point numbers are not abstract and are
difficult to refine and reason about. In this paper we present a refinement
calculus case study of the refinement of the real valued square root
function. We propose a general framework, based on interval arithmetic, for
the specification and refinement of real valued programs.
Conference Home Page