Deductive verification for programs using functional programming features

摘要

A processing device receives first specification information for an executable functional programming feature from a program and second specification information for the executable functional programming feature from a specification associated with the program. The processing device aggregates the first specification information with the second specification information to form combined specification information for the executable functional programming feature. The processing device verifies the executable programming feature using the combined specification information.