서브메뉴
검색
상세정보
A Balanced Verification Effort for the Java Language- [electronic resource]
![A Balanced Verification Effort for the Java Language - [electronic resource] / Zaccai, Die...](/Sponge/Images/bookDefaults/DDbookdefaultsmall.png)
A Balanced Verification Effort for the Java Language- [electronic resource]
상세정보
- 자료유형
- 학위논문(국외)
- 자관 청구기호
- 기본표목-개인명
- 표제와 책임표시사항
- A Balanced Verification Effort for the Java Language - [electronic resource] / Zaccai, Diego Sebastian.
- 발행, 배포, 간사 사항
- 발행, 배포, 간사 사항
- 형태사항
- 1 online resource(221 p)
- 일반주기
- Source: Dissertation Abstracts International, Volume: 78-04(E), Section: B.
- 일반주기
- Adviser: Bruce W. Weide.
- 학위논문주기
- Thesis (Ph.D.)--The Ohio State University, 2016.
- 요약 등 주기
- 요약Current tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing this long-standing verification problem try not to sacrifice modularity because modular reasoning is what makes verification tractable. To achieve this, these approaches treat the value of a reference variable as a memory address in the heap. A serious problem with this decision is that it severely limits the usefulness of generic collections because they must be specified as collections of references, and components of this kind are fundamentally flawed in design and implementation. The limitations become clear when attempting to verify clients of generic collections.
- 요약 등 주기
- 요약The first step in rectifying the situation is to redefine the "value" of a reference variable in terms of the abstract value of the object it references. A careful analysis of what the "value" of a reference variable might mean leads inevitably to this conclusion, which is consistent with the denotation of a variable in languages with value semantics, such as RESOLVE. Verification in languages with value semantics is straightforward compared to verification in languages with reference semantics precisely because of the lack of concern with heap properties. However, there is still a nagging problem: aliasing can occur in legal programs in languages with reference semantics, such as Java, and it must be handled when it does occur. The crux of the issue is not in-your-face assignment statements that copy references but rather aliasing arising within (hidden) method bodies. The reason is that the effects of calls to these methods in client code must be summarized in their specifications in order to preserve modularity.
- 요약 등 주기
- 요약So, the second step is the introduction of a discipline restricting what a client can do with a reference that is aliased within a method. The discipline advertises the creation of such aliases in method specifications and prevents a client from engaging in behavior that would break the abstractions of the objects being referenced, as this would also prevent modular verification. These restrictions allow code to be specified in terms of the abstract values of objects instead of treating the values of references as memory addresses in the heap. Even though the discipline prevents some programming idioms, it remains flexible enough to allow for most common programs, including the use of iterators, without the need for workarounds.
- 요약 등 주기
- 요약A tool can verify that a program satisfies the provisions of this discipline. Further, it can generate verification conditions that rely only on abstract object values to demonstrate a program(apostrophe)s correctness. These verification conditions can be discharged by the theorem-proving tools currently used to verify RESOLVE programs.
- 주제명부출표목-일반주제명
- 부출표목-단체명
- 기본자료저록
- Dissertation Abstracts International. 78-04B(E).
- 기본자료저록
- Dissertation Abstract International
- 전자적 위치 및 접속
- 원문정보보기
- 소장사항
-
20180515 2018
MARC
008180601s2016 us esm 001c eng■001MOKWON01261030
■00520180518092917
■007cr
■020 ▼a9781369371086
■035 ▼a(MiAaPQ)AAI10294708
■035 ▼a(MiAaPQ)OhioLINK:osu1461243619
■040 ▼aMiAaPQ▼cMiAaPQ
■090 ▼a전자도서(박사논문)
■1001 ▼aZaccai, Diego Sebastian.
■24512▼aA Balanced Verification Effort for the Java Language▼h[electronic resource]▼cZaccai, Diego Sebastian.
■260 ▼a[Sl]▼bThe Ohio State University▼c2016
■260 1▼aAnn Arbor▼bProQuest Dissertations & Theses▼c2016
■300 ▼a1 online resource(221 p)
■500 ▼aSource: Dissertation Abstracts International, Volume: 78-04(E), Section: B.
■500 ▼aAdviser: Bruce W. Weide.
■5021 ▼aThesis (Ph.D.)--The Ohio State University, 2016.
■520 ▼aCurrent tools used to verify software in languages with reference semantics, such as Java, are hampered by the possibility of aliases. Existing approaches to addressing this long-standing verification problem try not to sacrifice modularity because modular reasoning is what makes verification tractable. To achieve this, these approaches treat the value of a reference variable as a memory address in the heap. A serious problem with this decision is that it severely limits the usefulness of generic collections because they must be specified as collections of references, and components of this kind are fundamentally flawed in design and implementation. The limitations become clear when attempting to verify clients of generic collections.
■520 ▼aThe first step in rectifying the situation is to redefine the "value" of a reference variable in terms of the abstract value of the object it references. A careful analysis of what the "value" of a reference variable might mean leads inevitably to this conclusion, which is consistent with the denotation of a variable in languages with value semantics, such as RESOLVE. Verification in languages with value semantics is straightforward compared to verification in languages with reference semantics precisely because of the lack of concern with heap properties. However, there is still a nagging problem: aliasing can occur in legal programs in languages with reference semantics, such as Java, and it must be handled when it does occur. The crux of the issue is not in-your-face assignment statements that copy references but rather aliasing arising within (hidden) method bodies. The reason is that the effects of calls to these methods in client code must be summarized in their specifications in order to preserve modularity.
■520 ▼aSo, the second step is the introduction of a discipline restricting what a client can do with a reference that is aliased within a method. The discipline advertises the creation of such aliases in method specifications and prevents a client from engaging in behavior that would break the abstractions of the objects being referenced, as this would also prevent modular verification. These restrictions allow code to be specified in terms of the abstract values of objects instead of treating the values of references as memory addresses in the heap. Even though the discipline prevents some programming idioms, it remains flexible enough to allow for most common programs, including the use of iterators, without the need for workarounds.
■520 ▼aA tool can verify that a program satisfies the provisions of this discipline. Further, it can generate verification conditions that rely only on abstract object values to demonstrate a program(apostrophe)s correctness. These verification conditions can be discharged by the theorem-proving tools currently used to verify RESOLVE programs.
■590 ▼aSchool code: 0168.
■650 4▼aComputer science
■690 ▼a0984
■71020▼aThe Ohio State University▼bComputer Science and Engineering.
■7730 ▼tDissertation Abstracts International▼g78-04B(E).
■773 ▼tDissertation Abstract International
■790 ▼a0168
■791 ▼aPh.D.
■792 ▼a2016
■793 ▼aEnglish
■85640▼uhttp://www.riss.kr/pdu/ddodLink.do?id=T14820785▼nKERIS▼z이 자료의 원문은 한국교육학술정보원에서 제공합니다.
■980 ▼a20180515▼f2018
