Inferring Concise Specifications of APIs

dc.contributor.author Singleton, John
dc.contributor.author Rajan, Hridesh
dc.contributor.author Leavens, Gary
dc.contributor.author Rajan, Hridesh
dc.contributor.author Cok, David
dc.contributor.department Computer Science
dc.date 2019-07-12T13:39:42.000
dc.date.accessioned 2020-06-30T01:54:55Z
dc.date.available 2020-06-30T01:54:55Z
dc.date.copyright Tue Jan 01 00:00:00 UTC 2019
dc.date.issued 2019-05-16
dc.description.abstract <p>Modern software relies on libraries and uses them via application programming interfaces (APIs). Correct API usage as well as many software engineering tasks are enabled when APIs have formal specifications. In this work, we analyze the implementation of each method in an API to infer a formal postcondition. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. Our key idea is an algorithm that converts such exponentially large specifications into a form that is more concise and thus more usable. This is done by leveraging the structure of the specifications that result from the use of SP. We applied our technique to infer postconditions for over 2,300 methods in seven popular Java libraries. Our technique was able to infer specifications for 75.7% of these methods, each of which was verified using an Extended Static Checker. We also found that 84.6% of resulting specifications were less than 1/4 page (20 lines) in length. Our technique was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.</p>
dc.description.comments <p>This is a pre-print made available through arxiv, doi: <a href="https://arxiv.org/ct?url=https%3A%2F%2Fdx.doi.org%2F10.13140%2FRG.2.2.29027.40480&v=6b90f09e">10.13140/RG.2.2.29027.40480</a>.</p>
dc.format.mimetype application/pdf
dc.identifier archive/lib.dr.iastate.edu/cs_pubs/36/
dc.identifier.articleid 1035
dc.identifier.contextkey 14563210
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_pubs/36
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/19892
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/cs_pubs/36/2019_Rajan_InferringConcisePreprint.pdf|||Fri Jan 14 23:47:07 UTC 2022
dc.source.uri 10.13140/RG.2.2.29027.40480
dc.subject.disciplines Computer Sciences
dc.subject.disciplines Software Engineering
dc.title Inferring Concise Specifications of APIs
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isAuthorOfPublication 4e3f4631-9a99-4a4d-ab81-491621e94031
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
File
Original bundle
Now showing 1 - 1 of 1
Name:
2019_Rajan_InferringConcisePreprint.pdf
Size:
391.98 KB
Format:
Adobe Portable Document Format
Description:
Collections