Poster: An Algorithm And Tool To Infer Practical Postconditions

Keywords

JML; Predicate transformers; Specification inference

Abstract

Manually writing pre-And postconditions to document the behavior of a large library is a time-consuming task; what is needed is a way to automatically infer them. Conventional wisdom is that, if one has preconditions, then one can use the strongest postcondition predicate transformer (SP) to infer postconditions. However, we have performed a study using 2,300 methods in 7 popular Java libraries, and found that SP yields postconditions that are exponentially large, which makes them difficult to use, either by humans or by tools. We solve this problem using a novel algorithm and tool for inferring method postconditions, using the SP, and transmuting the inferred postconditions to make them more concise. 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 these inferred postconditions 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 algorithm was able to reduce the length of SMT proofs needed for verifying implementations by 76.7% and reduced prover execution time by 26.7%.

Publication Date

5-27-2018

Publication Title

Proceedings - International Conference on Software Engineering

Number of Pages

313-314

Document Type

Article; Proceedings Paper

Personal Identifier

scopus

DOI Link

https://doi.org/10.1145/3183440.3194986

Socpus ID

85049675010 (Scopus)

Source API URL

https://api.elsevier.com/content/abstract/scopus_id/85049675010

This document is currently not available here.

Share

COinS