Dissertation > Excellent graduate degree dissertation topics show

Axiomatic semantics of the Java language 's exception handling mechanism

Author: QuWenJing
Tutor: WangShuYi
School: Dalian University of Technology
Course: Applied Computer Technology
Keywords: exception handling mechanism of Java Java programming language axiomatic semantics program verification
CLC: TP312
Type: Master's thesis
Year: 2004
Downloads: 133
Quote: 0
Read: Download Dissertation

Abstract


In this thesis axiomatic semantics of Java exception handling mechanism is introduced. The contend of paper is divided into four parts: (1)Discuss the axiomatic semantics of throw and try statement.(2)Give the axiomatic semantics of the operator--new and continue, break andreturn statement, which are concerning about the exception handling. (3)We also give the axiomatic semantics of if statement and while statement and block statement in order to show that the axiomatic semantics plan is normal. (4)At last, we give an example of the correctness of code slice, which has the exception handling.About the axiomatic semantics, I have not see the articles about the axiomatic semantics of continue, break, return, and the main reason is these statements concerning about the control transfer and difficultly to describe the formula.To the exception handling mechanism, the axiomatic semantics is difficultly to research. The exception handling mechanism concerning large-scale control transfer, so the transfer is probably between the functions or files. When the exceptions happen, in the process of handling the exception, a series of function calling will terminate. To the control transfer, a variable REASON is introduced, which is recorded every state of statement execution. The states decide the control transfer. So, in every statement, the condition or conclusion of the axiomatic semantics of expression has the "REASON" . The condition of the REASON decide the axiom decide the next step of the program running. Describing the state of every point of code and adding some ruler, we can get the correctness of the program. Using the axiomatic semantics we solve the problem that describe the large-scale control transfer.

Related Dissertations

  1. Application and Research of Finite Element Method Among Lue Yang Electric Factory Slope Stability Analysis,TU43
  2. The Study on Network Planning and Optimization Technology of IP Core Networks,TN915.02
  3. Proof Generation for Certifying Compiler,TP314
  4. A Method to Generate Assertion and Proof about Assembly Language Certifying Compiler,TP314
  5. Verify with dynamic thread creation and exit multithreaded programs,TP311.53
  6. Analysis and Testing of Web Services Choreography Description Language,TP393.09
  7. A program verification tool design and implementation,TP311.53
  8. Analysis and Design of the Salary Module of Human Resource Management Information System,TP311.52
  9. Axiomatic Semantics of Class and Polymorphism for Java,TP312
  10. The Study and Development of the Simulation Programmer for NC Lathers,TG519.1
  11. Design and Implementation of Static Verifier in VeriJava,TP312.1
  12. Research on Methods of Security Assurance Based on Computer-Assisted Proof,TP309
  13. Study on Program Verification,TP311.11
  14. Verification of Low-level Concurrent Code with Several Synchronization Mechanisms,TP332
  15. Automated Loop Invariant Generation for Program Verification,TP311.11
  16. Verifying Parallel Programs Using Software Transactional Memory,TP311.5
  17. Program Verification Based on Computer Algebra,TP311.1
  18. Formal Semantics of Framed Temporal Logic Programming Language MSVL,TP312.1
  19. The Research of Partitioned Symbolic Execution Model and Its Environment Interaction Problem,TP311.11
  20. Study on Program Verification Based on Symbolic Computation,TP311.1

CLC: > Industrial Technology > Automation technology,computer technology > Computing technology,computer technology > Computer software > Programming language ALGOL
© 2012 www.DissertationTopic.Net  Mobile