Higher-order strategic programming: A road to software assurance

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. KEY WORDS program transformation, higher-order rules, distributed data problem, Java class loader, Sandia Secure Processor 1 Transformations The transformation of program structures through rewriting is an active area of research [2][3][6][7]. A primary goal is to enable rewriting to be used as a formal and automatable mechanism for high-assurance software development. Driving thi...

• Type: Conference
• Year: 2004
• Where: IASTEDSEA
• Authors: Victor L. Winter, Steve Roach, Fares Fraij
• Keywords: IASTEDSEA 2004, Program Transformation, Rewrite Rules, Simple Rewrite Rules, Software Engineering