Abstract

Program transformation through the repeated application of simple rewrite rules is conducive to formal verification. In practice, program transformation oftentimes requires data to be moved throughout the program structure. This article explores the use of higher-order rewrite rules as the mechanism for accomplishing such data movement. The effectiveness of higher-order rewrite rules is demonstrated by showing how they can be used to perform field distribution within a Java class loader. An approach to formal verification of a higher-order strategic implementation of a class loader is also briefly discussed.