Finding suitable programs: Semantic search with incomplete and lightweight specifications

Abstract—Finding suitable code for reuse is a common task for programmers. Two general approaches dominate the code search literature: syntactic and semantic. While queries for syntactic search are easy to compose, the results are often vague or irrelevant. On the other hand, a semantic search may return relevant results, but current techniques require developers to write specifications by hand, are costly as potentially matching code need to be executed to verify congruence with the specifi-cations, or only return exact matches. In this work, we propose an approach for semantic search in which programmers spec-ify lightweight, incomplete specifications and an SMT solver automatically identifies programs from a repository, encoded as constraints, that match the specifications. The repository of programs is automatically encoded offline so the search for matching programs is efficient. The program encodings cove