Axiomatic Semantics Of The Java Language Exception Handling Mechanism

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.