Modular verification of higher-order methods with mandatory calls specified by model programs Shaner, Steve
dc.contributor.department Computer Science 2018-02-14T00:55:22.000 2020-06-30T01:56:38Z 2020-06-30T01:56:38Z 2009-03-01
dc.description.abstract <p>Formal specification languages improve the flexibility and reliability of software. They capture program properties that can be verified against implementations of the specified program. By increasing the expressiveness of specification languages, we can strengthen the argument for adopting formal specification into standard programming practice. The higher-order method (HOM) is a kind of method whose behavior critically depends on one or more mandatory calls in its body. Programmers using HOMs would like to reason about the HOM's behavior, but revealing the entire code for such methods restricts writers of HOMs to a specific implementation. This thesis presents a simple, intuitive extension of JML, a formal specification language for Java, that enables client reasoning about the behavior of HOMs in a sound and modular way. Furthermore, our particular technique is capable of fully automatic checking with lower specification overhead than previous solutions. Supporting client reasoning about HOMs enables formal verification of some of the behavioral properties of HOM-using object-oriented design patterns, like Observer and Template Method. The technique also applies to specifying HOM behavior in any procedural language.</p>
dc.identifier archive/
dc.identifier.articleid 1323
dc.identifier.contextkey 5540262
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath cs_techreports/312
dc.source.bitstream archive/|||Fri Jan 14 23:31:35 UTC 2022
dc.subject.disciplines Programming Languages and Compilers
dc.subject.keywords Model program
dc.subject.keywords verification
dc.subject.keywords specification languages
dc.subject.keywords grey-box approach
dc.subject.keywords higher order method
dc.subject.keywords mandatory call
dc.subject.keywords Hoare logic
dc.subject.keywords refinement calculus
dc.title Modular verification of higher-order methods with mandatory calls specified by model programs
dc.type article
dc.type.genre article
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456
Original bundle
Now showing 1 - 1 of 1
308.59 KB
Adobe Portable Document Format