Product-line verification with feature-oriented contracts
Thomas Thüm · 2013
Software product lines allow programmers to reuse code across similar software products. Software products are decomposed into separate modules representing user-visible features. Based on a selection of desired features, a customized software product can be generated automatically. However, these reuse mechanisms challenge existing techniques for specification and verification of software. Specifying and verifying each product involves redundant steps, and is often infeasible. We discuss how method contracts (i.e., preconditions and postconditions) can be used to efficiently specify and verify product lines.