You are here

UCF Digital Collections ยป ETD Collection

reasoning about frame properties in object-oriented programs

Download pdf | Full Screen View

Date Issued:
2017
Abstract/Description:
Framing is important for specification and verification of object-oriented programs.This dissertation develops the local reasoning approach for framing in the presence of data structures with unrestricted sharing and subtyping.It can verify shared data structures specified in a concise way by unifying fine-grained region logic and separation logic. Then the fine-grained region logic is extended to reason about subtyping.First, fine-grained region logic is adapted from region logic to express regions at the granularity of individual fields. Conditional region expressions are introduced; not only does this allow one to specify more precise frame conditions, it also has the ability to express footprints of separation logic assertions.Second, fine-grained region logic is generalized to a new logic called unified fine-grained region logic by allowing the logic to restrict the heap in which a program runs. This feature allows one to express specifications in separation logic.Third, both fine-grained region logic and separation logic can be encoded to unified fine-grained region logic. This result allows the proof system to reason about programs specified in both styles.Finally, fine-grained region logic is extended to reason about a programming language that is similar to Java. To reason about inheritance locally, a frame condition for behavioral subtyping is defined and proved sound.
Title: reasoning about frame properties in object-oriented programs.
57 views
22 downloads
Name(s): Bao, Yuyan, Author
Leavens, Gary, Committee Chair
Dechev, Damian, Committee Member
Jha, Sumit Kumar, Committee Member
Cash, Mason, Committee Member
University of Central Florida, Degree Grantor
Type of Resource: text
Date Issued: 2017
Publisher: University of Central Florida
Language(s): English
Abstract/Description: Framing is important for specification and verification of object-oriented programs.This dissertation develops the local reasoning approach for framing in the presence of data structures with unrestricted sharing and subtyping.It can verify shared data structures specified in a concise way by unifying fine-grained region logic and separation logic. Then the fine-grained region logic is extended to reason about subtyping.First, fine-grained region logic is adapted from region logic to express regions at the granularity of individual fields. Conditional region expressions are introduced; not only does this allow one to specify more precise frame conditions, it also has the ability to express footprints of separation logic assertions.Second, fine-grained region logic is generalized to a new logic called unified fine-grained region logic by allowing the logic to restrict the heap in which a program runs. This feature allows one to express specifications in separation logic.Third, both fine-grained region logic and separation logic can be encoded to unified fine-grained region logic. This result allows the proof system to reason about programs specified in both styles.Finally, fine-grained region logic is extended to reason about a programming language that is similar to Java. To reason about inheritance locally, a frame condition for behavioral subtyping is defined and proved sound.
Identifier: CFE0007279 (IID), ucf:52195 (fedora)
Note(s): 2017-12-01
Ph.D.
Engineering and Computer Science, Computer Science
Doctoral
This record was generated from author submitted information.
Subject(s): separation logic -- region logic -- fine-grained region logic -- framing -- shared mutable data structure -- formal specification -- formal verification -- Hoare logic -- unified fine-grained region logic
Persistent Link to This Record: http://purl.flvc.org/ucf/fd/CFE0007279
Restrictions on Access: public 2018-06-15
Host Institution: UCF

In Collections