Learning Program Specifications from Sample Runs