Second-Order Programs with Preconditions

Abstract. In the implementation of procedures, developers often assume that the input satisfies certain properties; for example, binary search assumes the array to be sorted. Such requirements on the input can be formally expressed as preconditions of procedures. If a secondorder procedure p (e.g., map or foldl) is called with a first-order procedure f that has a precondition, the question arises whether p will call f only with arguments that satisfy the precondition of f. In this paper, we propose a method to statically analyze if all procedure calls in a given second-order program satisfy the respective preconditions. In particular, we consider indirect calls of procedures that are passed as an argument to a second-order procedure.

• Type: Journal
• Year: 2010
• Where: BIRTHDAY
• Authors: Markus Aderhold
• Keywords: Applied Computing, BIRTHDAY 2010, Certain Properties, Preconditions, Procedure