Author(s)

M. Harman & S. Danicic

Abstract

DeMillo, Lipton and Perils [4] and Fetzer [7] have argued that one significant reason for the inapplicability of formal verification techniques such as the Axiomatic Method of Hoare [13] and Dijkstra[5], is the sheer size of real software systems. In this paper we argue that slicing offers a way to overcome this difficulty opening up the way to a 'slice-and-verify' approach to guaranteeing software quality. Slicing, introduced by Weiser in [21, 22] and extended in [17, 1, 8, 10], is a technique for simplifying programs by focusing upon subcomponents of their computation. Since a slice is guaranteed to preserve the original program's effect with respect to a given set of variables, verification of the slice automatically 'carries over' to the overall program from

Keywords